Subst (soteria-c.Soteria_c_lib.Ctree

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 Soteria.Bv_values.Bv_solver.Z3_solver.Value.ty ->
      'a Soteria.Bv_values.Bv_solver.Z3_solver.Value.t) ->
  t ->
  t ->
  'a Soteria.Bv_values.Bv_solver.Z3_solver.Value.t * t

val learn : 
  t ->
  t ->
  'a Soteria.Bv_values.Bv_solver.Z3_solver.Value.t ->
  t option