Parameter Make.L

val name : string

Name of the encoding. Used only for debugging.

type internal
val init : SL.t -> HeapSort.t -> LocationBounds0.t -> t
val var_axiom : t -> SMT.Variable.t -> SMT.t
val heap_axioms : t -> SMT.t -> SMT.t
val lemmas : t -> SMT.t
val show : t -> string