val initializations : t -> int Bitvector.Collection.Map.tval create : unit -> tval assign : ?wild:bool -> string -> Formula.sort -> Formula.term -> t -> tval havoc : ?wild:bool -> string -> Formula.sort -> t -> tassign variable with a fresh symbolic value
val declare : ?wild:bool -> string -> Formula.sort -> t -> tif wild is set, then the variable is appended to uncontroled
val constrain : Formula.bl_term -> t -> tconstrain c s adds constraint c to state s
val formula : t -> Formula.formulaval memory_term : Formula.ax_term -> string * Formula.sort * Formula.termval get_memory : t -> Formula.ax_termval get_path_constraint : t -> Formula.bl_termval get_bv : string -> Size.Bit.t -> t -> Formula.bv_term * tautomatically declares missing variables, thus returns t
val init_mem_at : addr:Bitvector.t -> size:int -> t -> tval uncontrolled : t -> Formula.VarSet.tval pp : Format.formatter -> t -> unit