Expr.Subst
type t = Soteria.Bv_values.Bv_solver.Z3_solver.Value.Expr.Subst.t
val pp : Stdlib.Format.formatter -> t -> unit
val empty : t
val apply : missing_var:(Soteria.Symex.Var.t -> 'a ty -> 'a t) -> t -> t -> 'a t * t
val learn : t -> t -> 'a t -> t option