From 0af0d3b210a4a55838e86fb0df9254f29c223bc6 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Fri, 8 Mar 2019 07:07:19 -0800 Subject: [PATCH] [sledge] Revise Equality carrier-closure invariant Summary: Interpreted subexps were not handled correctly: they must not be in the carrier, but their non-interpreted subexps should. Reviewed By: jvillard Differential Revision: D14344291 fbshipit-source-id: 995896640 --- sledge/src/symbheap/equality.ml | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/sledge/src/symbheap/equality.ml b/sledge/src/symbheap/equality.ml index f3bca2a1e..8b30a2a9f 100644 --- a/sledge/src/symbheap/equality.ml +++ b/sledge/src/symbheap/equality.ml @@ -82,6 +82,11 @@ let pp_diff fs (r, s) = (** test membership in carrier *) let in_car r e = Map.mem r.rep e +let rec iter_max_solvables e ~f = + match Exp.classify e with + | `Interpreted -> Exp.iter ~f:(iter_max_solvables ~f) e + | _ -> f e + let invariant r = Invariant.invariant [%here] r [%sexp_of: t] @@ fun () -> @@ -89,7 +94,7 @@ let invariant r = (* no interpreted exps in carrier *) assert (Poly.(Exp.classify a <> `Interpreted)) ; (* carrier is closed under sub-expressions *) - Exp.iter a ~f:(fun b -> + iter_max_solvables a ~f:(fun b -> assert ( in_car r b || Trace.fail "@[subexp %a of %a not in carrier of@ %a@]" Exp.pp