Fix tests.

Author: gebner

test/bug-reports/Bug.SpinLock.fst.output.expected

@@ -1,5 +1,6 @@
 * Info at Bug.SpinLock.fst(45,2-45,4):
   - Expected failure:
+  - Tactic failed
   - Cannot prove:
       Pulse.Lib.Reference.pts_to __ ?__
   - In the context:

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

@@ -1,8 +1,10 @@
 * Info at Bug107.fst(45,9-45,16):
   - Expected failure:
+  - Tactic failed
   - Could not resolve implicit uu___#87 of type Prims.int in term Bug107.foo 1 _
 
 * Info at Bug107.fst(56,9-56,16):
   - Expected failure:
+  - Tactic failed
   - Could not resolve implicit uu___#87 of type Prims.int in term Bug107.foo _ 2
 

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

@@ -1,5 +1,6 @@
 * Info at Bug267.fst(14,4-14,6):
   - Expected failure:
+  - Tactic failed
   - Expected a total term, but this term has Ghost effect
 
 * Info at Bug267.fst(62,4-62,5):

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

@@ -1,5 +1,6 @@
 * Info at Bug274.fst(29,4-29,15):
   - Expected failure:
+  - Tactic failed
   - Cannot prove any of:
       Pulse.Lib.Trade.trade _ _ ** Pulse.Lib.Trade.trade _ _
   - In the context:
@@ -36,6 +37,7 @@
 
 * Info at Bug274.fst(41,4-41,15):
   - Expected failure:
+  - Tactic failed
   - Cannot prove any of:
       Pulse.Lib.Trade.trade _ _ ** Pulse.Lib.Trade.trade _ _
   - In the context:
@@ -72,6 +74,7 @@
 
 * Info at Bug274.fst(73,4-73,12):
   - Expected failure:
+  - Tactic failed
   - Cannot prove any of:
       _ ** Pulse.Lib.Trade.trade _ _
   - In the context:

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

@@ -1,5 +1,6 @@
 * Info at Bug29.fst(57,4-57,45):
   - Expected failure:
+  - Tactic failed
   - Cannot prove:
       Pulse.Lib.Reference.pts_to r v
   - In the context:

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

@@ -1,10 +1,12 @@
 * Info at ExistsErasedAndPureEqualities.fst(32,4-33,21):
   - Expected failure:
+  - Tactic failed
   - Could not resolve all free variables in the proposition: v == v_
   - See also ExistsErasedAndPureEqualities.fst(32,4-34,12)
 
 * Info at ExistsErasedAndPureEqualities.fst(50,4-51,21):
   - Expected failure:
+  - Tactic failed
   - Could not resolve all free variables in the proposition: v == v_
   - See also ExistsErasedAndPureEqualities.fst(50,4-52,12)
 
@@ -21,6 +23,7 @@
 
 * Info at ExistsErasedAndPureEqualities.fst(79,4-80,21):
   - Expected failure:
+  - Tactic failed
   - Could not resolve all free variables in the proposition: v == v_
   - See also ExistsErasedAndPureEqualities.fst(79,4-81,12)
 

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

@@ -1,12 +1,14 @@
 * Info at IntroGhost.fst(44,18-44,20):
   - Expected failure:
+  - Tactic failed
   - Cannot prove:
       Pulse.Lib.Reference.pts_to r __
   - In the context:
       IntroGhost.my_inv b r
 
 * Info at IntroGhost.fst(71,2-71,4):
   - Expected failure:
+  - Tactic failed
   - Cannot prove:
       Pulse.Lib.Reference.pts_to r 0
   - In the context:

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

@@ -1,10 +1,12 @@
 * Info at PartialApp.fst(26,2-26,3):
   - Expected failure:
+  - Tactic failed
   - This statement returns a value of type: Prims.int
   - Did you forget to assign it or ignore it?
 
 * Info at PartialApp.fst(60,2-60,9):
   - Expected failure:
+  - Tactic failed
   - This function is partially applied. Remaining type:
       y: t
         -> Pulse.Lib.Core.stt Prims.unit

test/nolib/Test.Matcher.fst.output.expected

@@ -1,5 +1,6 @@
 * Info at Test.Matcher.fst(69,2-69,4):
   - Expected failure:
+  - Tactic failed
   - Cannot prove:
       Test.Matcher.fpts_to #Prims.int
         r

test/nolib/Test.RewriteBy.fst.output.expected

@@ -12,5 +12,5 @@
   - Reduction stopped at:
       reify (let _ = FStar.Stubs.Tactics.V2.Builtins.dump "a" in
           Test.RewriteBy.tac ())
-        "(((proofstate)))"
+        "(((ref proofstate)))"