[sledge] Fix: Sh.pure

Summary:
It was incorrect in case any but the first of of the Formula.disjuncts
was inconsistent.

Reviewed By: ngorogiannis

Differential Revision: D23459519

fbshipit-source-id: 394677e38

sledge/src/sh.ml

@@ -526,7 +526,7 @@ let pure (p : Formula.t) =
     ~f:(fun q p ->
       let us = Formula.fv p in
       let xs, ctx = Context.add us p Context.empty in
-      if Context.is_unsat ctx then false_ us
+      if Context.is_unsat ctx then extend_us us q
       else or_ q (exists_fresh xs {emp with us; ctx; pure= p}) )
   |>
   [%Trace.retn fun {pf} q ->