Fix tests.

Author: gebner

test/LoopInvariants.fst.output.expected

@@ -2,23 +2,23 @@
   - Expected failure:
   - When using multiple invariants, they must all be in the "new" style without a binder.
 
-* Info at LoopInvariants.fst(77,4-77,8):
+* Info at LoopInvariants.fst(76,20-77,8):
   - Expected failure:
-  - rewrite: could not prove equality of
+  - Could not prove equality of:
   - Pulse.Lib.Reference.pts_to s 3
   - Pulse.Lib.Reference.pts_to s 2
   - Assertion failed
   - The SMT solver could not prove the query. Use --query_stats for more
     details.
-  - See also LoopInvariants.fst(77,4-77,10)
+  - See also LoopInvariants.fst(76,20-77,10)
 
-* Info at LoopInvariants.fst(88,4-88,8):
+* Info at LoopInvariants.fst(86,2-88,8):
   - Expected failure:
-  - rewrite: could not prove equality of
+  - Could not prove equality of:
   - Pulse.Lib.Reference.pts_to s 3
   - Pulse.Lib.Reference.pts_to s 2
   - Assertion failed
   - The SMT solver could not prove the query. Use --query_stats for more
     details.
-  - See also LoopInvariants.fst(88,4-88,10)
+  - See also LoopInvariants.fst(86,2-88,10)
 

test/bug-reports/Bug174.fst.output.expected

@@ -1,9 +1,14 @@
-* Info at Bug174.fst(15,1-16,42):
+* Info at Bug174.fst(16,30-16,42):
   - Expected failure:
-  - rewrite: could not prove equality of
-  - Pulse.Lib.Reference.pts_to r v
-  - Pulse.Lib.Reference.pts_to r v
+  - Ill-typed term: !r
+  - Expected a term of type
+      Pulse.Lib.Core.stt FStar.SizeT.t
+        (r |-> Pulse.Class.PtsTo.Frac 1.0R v)
+        (fun x ->
+            r |-> Pulse.Class.PtsTo.Frac 1.0R v **
+            Pulse.Lib.Core.rewrites_to x v)
   - Assertion failed
   - The SMT solver could not prove the query. Use --query_stats for more
     details.
+  - See also Bug174.fst(15,1-16,40)
 

test/bug-reports/ExistsErasedAndPureEqualities.fst.output.expected

@@ -9,9 +9,9 @@
       v#269 : FStar.Ghost.erased Prims.int,
       x#263 : Pulse.Lib.Reference.ref Prims.int
 
-* Info at ExistsErasedAndPureEqualities.fst(70,4-71,21):
+* Info at ExistsErasedAndPureEqualities.fst(70,32-72,5):
   - Expected failure:
-  - Failed to prove pure property: v == (*?u102*)_
+  - Ill-typed term: pure (v == (*?u102*)_)
+  - Expected a term of type slprop
   - Cannot check relation with uvars.
-  - See also ExistsErasedAndPureEqualities.fst(70,23-71,15)