diff --git a/sledge/src/sh.ml b/sledge/src/sh.ml index 9ed676237..4b18e279b 100644 --- a/sledge/src/sh.ml +++ b/sledge/src/sh.ml @@ -595,9 +595,13 @@ let rec is_empty q = let rec pure_approx q = Formula.andN - ( q.pure - :: List.map q.djns ~f:(fun djn -> - Formula.orN (List.map djn ~f:pure_approx) ) ) + ( [q.pure] + |> fun init -> + List.fold ~init q.heap ~f:(fun p seg -> + Formula.dq Term.zero seg.loc :: p ) + |> fun init -> + List.fold ~init q.djns ~f:(fun p djn -> + Formula.orN (List.map djn ~f:pure_approx) :: p ) ) let pure_approx q = [%Trace.call fun {pf} -> pf "%a" pp q]