[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

@@ -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