diff --git a/sledge/src/symbheap/domain.ml b/sledge/src/symbheap/domain.ml index 69697f6c4..1d2b90533 100644 --- a/sledge/src/symbheap/domain.ml +++ b/sledge/src/symbheap/domain.ml @@ -19,7 +19,6 @@ let init globals = Sh.star q (Sh.seg {loc; bas= loc; len; siz= len; arr}) | _ -> q ) -let bottom = Sh.false_ Var.Set.empty let join = Sh.or_ let assume q b = Exec.assume b q let exec_inst = Exec.inst diff --git a/sledge/src/symbheap/domain.mli b/sledge/src/symbheap/domain.mli index a8e28997d..ee20df904 100644 --- a/sledge/src/symbheap/domain.mli +++ b/sledge/src/symbheap/domain.mli @@ -11,7 +11,6 @@ type t val pp : t pp val init : Global.t vector -> t -val bottom : t val join : t -> t -> t val assume : t -> Exp.t -> t option val exec_inst : t -> Llair.inst -> (t, t * Llair.inst) result