nudge an example

Author: nikswamy

lib/pulse/lib/Pulse.Lib.Swap.Slice.fst

@@ -73,7 +73,7 @@ fn slice_swap_aux(#t: Type0) (a: S.slice t) (mb: (mb: SZ.t {0 < SZ.v mb /\ SZ.v
         S.op_Array_Assignment a idx x;
         pj := j';
         pidx := idx';
-        ()
+        #set-options "--z3refresh" { () } //restart the solver to prove the invariant at the end in a clean state
       };
       ();
       with s . assert (pts_to a s);

src/checker/Pulse.Checker.Prover.fst

@@ -625,7 +625,7 @@ let prove_atom (g: env) (ctxt: list slprop_view) (allow_amb: bool) (goal: slprop
         with_uf_transaction (fun _ ->
           match mkeys, mkeys' with
           | Some mkeys, Some mkeys' ->
-            T.zip mkeys mkeys' |> forallb (fun (a, b) -> RU.teq_nosmt_force (elab_env g) a b)
+            T.zip mkeys mkeys' |> forallb (fun (a, b) -> RU.teq_nosmt_force_phase1 (elab_env g) a b)
           | _, _ ->
             teq_nosmt_force_args (elab_env g) ctxt goal true
         )