Update expected error output, after F* patch

mtzguido · mtzguido · commit d4be0c9688ac · 2025-08-14T10:26:59.000-07:00
FStarLang/FStar#3972
diff --git a/test/MatchBasic.fst.output.expected b/test/MatchBasic.fst.output.expected
@@ -1,10 +1,9 @@
->> Got issues: [
-* Error 19 at MatchBasic.fst(154,2-156,3):
+* Info at MatchBasic.fst(154,2-156,3):
+  - Expected failure:
   - Could not verify that this match is exhaustive.
   - Patterns are incomplete
   - The SMT solver could not prove the query. Use --query_stats for more
     details.
   - Also see: MatchBasic.fst(154,8-154,10)
   - Other related locations: dummy(0,0-0,0)
 
->>]
diff --git a/test/Test.Recursion.fst.output.expected b/test/Test.Recursion.fst.output.expected
@@ -1,5 +1,5 @@
->> Got issues: [
-* Error 19 at Test.Recursion.fst(94,2-94,20):
+* Info at Test.Recursion.fst(94,2-94,20):
+  - Expected failure:
   - Ill-typed term: ()
   - Expected a term of type
       x':
@@ -11,9 +11,8 @@
   - The SMT solver could not prove the query. Use --query_stats for more
     details.
 
->>]
->> Got issues: [
-* Error 19 at Test.Recursion.fst(141,4-141,22):
+* Info at Test.Recursion.fst(141,4-141,22):
+  - Expected failure:
   - Ill-typed term: y - 1
   - Expected a term of type
       y':
@@ -25,4 +24,3 @@
   - The SMT solver could not prove the query. Use --query_stats for more
     details.
 
->>]
diff --git a/test/bug-reports/Bug.DesugaringError.fst.output.expected b/test/bug-reports/Bug.DesugaringError.fst.output.expected
@@ -1,22 +1,18 @@
->> Got issues: [
-* Error 72 at Bug.DesugaringError.fst(11,4-11,5):
+* Info at Bug.DesugaringError.fst(11,4-11,5):
+  - Expected failure:
   - Identifier not found: a
   - Hint: Did you mean x or y?
 
->>]
->> Got issues: [
-* Error 72 at Bug.DesugaringError.fst(16,12-16,21):
+* Info at Bug.DesugaringError.fst(16,12-16,21):
+  - Expected failure:
   - Identifier not found: something
 
->>]
->> Got issues: [
-* Error 189 at Bug.DesugaringError.fst(31,9-31,10):
+* Info at Bug.DesugaringError.fst(31,9-31,10):
+  - Expected failure:
   - Expected expression of type Prims.nat got expression y of type Prims.bool
   - See also Bug.DesugaringError.fst(31,4-31,10)
 
->>]
->> Got issues: [
-* Error 189 at Bug.DesugaringError.fst(46,4-46,8):
+* Info at Bug.DesugaringError.fst(46,4-46,8):
+  - Expected failure:
   - Expected expression of type Prims.nat got expression true of type Prims.bool
 
->>]
diff --git a/test/bug-reports/Bug.SpinLock.fst.output.expected b/test/bug-reports/Bug.SpinLock.fst.output.expected
@@ -1,9 +1,8 @@
->> Got issues: [
-* Error 228 at Bug.SpinLock.fst(45,2-45,4):
+* Info at Bug.SpinLock.fst(45,2-45,4):
+  - Expected failure:
   - Cannot prove:
       Pulse.Lib.Reference.pts_to _ ?uu___
   - In the context:
       Pulse.Lib.SpinLock.lock_alive my_lock
         (exists* (v: Prims.int). Pulse.Lib.Reference.pts_to r v)
 
->>]
diff --git a/test/bug-reports/Bug100.fst.output.expected b/test/bug-reports/Bug100.fst.output.expected
@@ -1,30 +1,27 @@
->> Got issues: [
-* Error 19 at Bug100.fst(10,31-10,33):
+* Info at Bug100.fst(10,31-10,33):
+  - Expected failure:
   - Subtyping check failed
   - Expected type FStar.Seq.Base.seq Prims.int
     got type FStar.Seq.Base.seq Prims.nat
   - The SMT solver could not prove the query. Use --query_stats for more
     details.
   - See also Prims.fst(682,18-682,24)
 
->>]
->> Got issues: [
-* Error 19 at Bug100.fst(19,57-19,58):
+* Info at Bug100.fst(19,57-19,58):
+  - Expected failure:
   - Subtyping check failed
   - Expected type FStar.Seq.Base.seq Prims.int
     got type FStar.Seq.Base.seq Prims.nat
   - The SMT solver could not prove the query. Use --query_stats for more
     details.
   - See also Prims.fst(682,18-682,24)
 
->>]
->> Got issues: [
-* Error 19 at Bug100.fst(23,11-23,17):
+* Info at Bug100.fst(23,11-23,17):
+  - Expected failure:
   - Ill-typed term: Bug100.pts_to Prims.int a1 s1
   - Expected a term of type slprop
   - Assertion failed
   - The SMT solver could not prove the query. Use --query_stats for more
     details.
   - Also see: Prims.fst(161,28-183,79)
 
->>]
diff --git a/test/bug-reports/Bug107.fst.output.expected b/test/bug-reports/Bug107.fst.output.expected
@@ -1,14 +1,12 @@
->> Got issues: [
-* Error 228 at Bug107.fst(45,9-45,16):
+* Info at Bug107.fst(45,9-45,16):
+  - Expected failure:
   - Could not resolve implicit uu___#194
     of type Prims.int
     in term Bug107.foo 1 _
 
->>]
->> Got issues: [
-* Error 228 at Bug107.fst(56,9-56,16):
+* Info at Bug107.fst(56,9-56,16):
+  - Expected failure:
   - Could not resolve implicit uu___#194
     of type Prims.int
     in term Bug107.foo _ 2
 
->>]
diff --git a/test/bug-reports/Bug111.fst.output.expected b/test/bug-reports/Bug111.fst.output.expected
@@ -1,6 +1,5 @@
->> Got issues: [
-* Error 114 at Bug111.fst(13,2-20,3):
+* Info at Bug111.fst(13,2-20,3):
+  - Expected failure:
   - Could not verify that this match is exhaustive.
   - Type of pattern (Prims.int) does not match type of scrutinee (FStar.Ghost.erased Prims.int)
 
->>]
diff --git a/test/bug-reports/Bug113.fst.output.expected b/test/bug-reports/Bug113.fst.output.expected
@@ -1,5 +1,4 @@
->> Got issues: [
-* Error 72 at Bug113.fst(29,38-29,44):
+* Info at Bug113.fst(29,38-29,44):
+  - Expected failure:
   - Identifier not found: erased
 
->>]
diff --git a/test/bug-reports/Bug169.fst.output.expected b/test/bug-reports/Bug169.fst.output.expected
@@ -1,5 +1,4 @@
->> Got issues: [
-* Error 72 at Bug169.fst(10,24-10,29):
+* Info at Bug169.fst(10,24-10,29):
+  - Expected failure:
   - Module name SiveT could not be resolved.
 
->>]
diff --git a/test/bug-reports/Bug174.fst.output.expected b/test/bug-reports/Bug174.fst.output.expected
@@ -1,5 +1,5 @@
->> Got issues: [
-* Error 19 at Bug174.fst(16,10-16,42):
+* Info at Bug174.fst(16,10-16,42):
+  - Expected failure:
   - Ill-typed term: !r
   - Assertion failed
   - The SMT solver could not prove the query. Use --query_stats for more
@@ -8,4 +8,3 @@
   - Other related locations: Bug174.fst(16,39-16,40)
   - See also Bug174.fst(15,1-17,10)
 
->>]
diff --git a/test/bug-reports/Bug206.fst.output.expected b/test/bug-reports/Bug206.fst.output.expected
@@ -1,5 +1,5 @@
->> Got issues: [
-* Error 19 at Bug206.fst(18,7-18,8):
+* Info at Bug206.fst(18,7-18,8):
+  - Expected failure:
   - Ill-typed term: x
   - Expected a term of type x: Prims.nat{x > 0}
   - Assertion failed
@@ -9,4 +9,3 @@
   - Other related locations: Bug206.fst(6,20-6,20)
   - See also Bug206.fst(18,2-18,8)
 
->>]
diff --git a/test/bug-reports/Bug266.fst.output.expected b/test/bug-reports/Bug266.fst.output.expected
@@ -1,12 +1,11 @@
->> Got issues: [
-* Error 19 at Bug266.fst(12,2-12,14):
+* Info at Bug266.fst(12,2-12,14):
+  - Expected failure:
   - Failed to prove pure property: Prims.l_False
   - Assertion failed
   - The SMT solver could not prove the query. Use --query_stats for more
     details.
   - See also Bug266.fst(12,31-12,36)
 
->>]
 * Info at Bug266.fst(28,2-28,9):
   - Admitting continuation.
   - Current context:
diff --git a/test/bug-reports/Bug267.fst.output.expected b/test/bug-reports/Bug267.fst.output.expected
@@ -1,10 +1,9 @@
->> Got issues: [
-* Error 228 at Bug267.fst(14,4-14,6):
+* Info at Bug267.fst(14,4-14,6):
+  - Expected failure:
   - Expected a total term, but this term has Ghost effect
 
->>]
->> Got issues: [
-* Error 19 at Bug267.fst(62,4-62,5):
+* Info at Bug267.fst(62,4-62,5):
+  - Expected failure:
   - Could not prove equality between computed type Prims.int
     and expected type Prims.nat
   - Assertion failed
@@ -13,9 +12,7 @@
   - Also see: Prims.fst(161,28-183,79)
   - See also Bug267.fst(62,4-62,8)
 
->>]
->> Got issues: [
-* Error 12 at Bug267.fst(67,13-67,14):
+* Info at Bug267.fst(67,13-67,14):
+  - Expected failure:
   - Expected type Pulse.Lib.Core.slprop but n >= 1 has type Prims.bool
 
->>]
diff --git a/test/bug-reports/Bug274.fst.output.expected b/test/bug-reports/Bug274.fst.output.expected
@@ -1,5 +1,5 @@
->> Got issues: [
-* Error 228 at Bug274.fst(29,4-29,15):
+* Info at Bug274.fst(29,4-29,15):
+  - Expected failure:
   - Cannot prove any of:
       Pulse.Lib.Trade.trade _ _ ** Pulse.Lib.Trade.trade _ _
   - In the context:
@@ -34,9 +34,8 @@
       Pulse.Lib.Trade.trade q r
     in the context.
 
->>]
->> Got issues: [
-* Error 228 at Bug274.fst(41,4-41,15):
+* Info at Bug274.fst(41,4-41,15):
+  - Expected failure:
   - Cannot prove any of:
       Pulse.Lib.Trade.trade _ _ ** Pulse.Lib.Trade.trade _ _
   - In the context:
@@ -71,9 +70,8 @@
       Pulse.Lib.Trade.trade p q
     in the context.
 
->>]
->> Got issues: [
-* Error 228 at Bug274.fst(73,4-73,12):
+* Info at Bug274.fst(73,4-73,12):
+  - Expected failure:
   - Cannot prove any of:
       _ ** Pulse.Lib.Trade.trade _ _
   - In the context:
@@ -108,4 +106,3 @@
       p
     in the context.
 
->>]
diff --git a/test/bug-reports/Bug278.fst.output.expected b/test/bug-reports/Bug278.fst.output.expected
@@ -1,5 +1,4 @@
->> Got issues: [
-* Error 339 at Bug278.fst(36,11-36,56):
+* Info at Bug278.fst(36,11-36,56):
+  - Expected failure:
   - Elaborated term has unresolved univ uvars: Bug278.spawn (Bug278.pth n)
 
->>]
diff --git a/test/bug-reports/Bug29.fst.output.expected b/test/bug-reports/Bug29.fst.output.expected
@@ -1,8 +1,7 @@
->> Got issues: [
-* Error 228 at Bug29.fst(57,4-57,45):
+* Info at Bug29.fst(57,4-57,45):
+  - Expected failure:
   - Cannot prove:
       Pulse.Lib.Reference.pts_to r v
   - In the context:
       emp
 
->>]
diff --git a/test/bug-reports/Bug36.fst.output.expected b/test/bug-reports/Bug36.fst.output.expected
@@ -1,6 +1,5 @@
->> Got issues: [
-* Error 189 at Bug36.fst(13,6-13,7):
+* Info at Bug36.fst(13,6-13,7):
+  - Expected failure:
   - Expected expression of type Type got expression n of type Prims.nat
   - See also Bug36.fst(13,2-13,7)
 
->>]
diff --git a/test/bug-reports/Bug45.fst.output.expected b/test/bug-reports/Bug45.fst.output.expected
@@ -1,5 +1,4 @@
->> Got issues: [
-* Error 339 at Bug45.fst(64,13-64,58):
+* Info at Bug45.fst(64,13-64,58):
+  - Expected failure:
   - Elaborated term has unresolved univ uvars: Bug45.spawn (Bug45.pth n)
 
->>]
diff --git a/test/bug-reports/Bug59.fst.output.expected b/test/bug-reports/Bug59.fst.output.expected
@@ -1,9 +1,8 @@
->> Got issues: [
-* Error 19 at Bug59.fst(12,11-12,24):
+* Info at Bug59.fst(12,11-12,24):
+  - Expected failure:
   - Ill-typed term: pure (x == y)
   - Expected a term of type slprop
   - Assertion failed
   - The SMT solver could not prove the query. Use --query_stats for more
     details.
 
->>]
diff --git a/test/bug-reports/Bug94.fst.output.expected b/test/bug-reports/Bug94.fst.output.expected
@@ -1,24 +1,21 @@
->> Got issues: [
-* Error 19 at Bug94.fst(11,16-11,18):
+* Info at Bug94.fst(11,16-11,18):
+  - Expected failure:
   - Ill-typed term: - 1
   - Expected a term of type Prims.nat
   - Assertion failed
   - The SMT solver could not prove the query. Use --query_stats for more
     details.
   - Also see: Prims.fst(682,18-682,24)
 
->>]
->> Got issues: [
-* Error 189 at Bug94.fst(20,16-20,17):
+* Info at Bug94.fst(20,16-20,17):
+  - Expected failure:
   - Expected expression of type Prims.nat got expression y of type Prims.string
   - See also Bug94.fst(19,1-21,4)
 
->>]
->> Got issues: [
-* Error 19 at Bug94.fst(36,18-36,27):
+* Info at Bug94.fst(36,18-36,27):
+  - Expected failure:
   - Ill-typed term: hundred 0
   - Assertion failed
   - The SMT solver could not prove the query. Use --query_stats for more
     details.
 
->>]
diff --git a/test/bug-reports/BugHigherOrderApplication.fst.output.expected b/test/bug-reports/BugHigherOrderApplication.fst.output.expected
@@ -1,7 +1,6 @@
->> Got issues: [
-* Error 228 at BugHigherOrderApplication.fst(197,4-197,7):
+* Info at BugHigherOrderApplication.fst(197,4-197,7):
+  - Expected failure:
   - Expected an arrow type; but head BugHigherOrderApplication.g has type f:
     (_: Prims.bool -> Pulse.Lib.Core.stt Prims.bool Pulse.Lib.Core.emp (fun _ -> Pulse.Lib.Core.emp))
       {f == f}
 
->>]
diff --git a/test/bug-reports/ExistsErasedAndPureEqualities.fst.output.expected b/test/bug-reports/ExistsErasedAndPureEqualities.fst.output.expected
@@ -1,15 +1,13 @@
->> Got issues: [
-* Error 228 at ExistsErasedAndPureEqualities.fst(32,4-33,21):
+* Info at ExistsErasedAndPureEqualities.fst(32,4-33,21):
+  - Expected failure:
   - Could not resolve all free variables in the proposition: v == v_
   - See also ExistsErasedAndPureEqualities.fst(32,4-34,12)
 
->>]
->> Got issues: [
-* Error 228 at ExistsErasedAndPureEqualities.fst(50,4-51,21):
+* Info at ExistsErasedAndPureEqualities.fst(50,4-51,21):
+  - Expected failure:
   - Could not resolve all free variables in the proposition: v == v_
   - See also ExistsErasedAndPureEqualities.fst(50,4-52,12)
 
->>]
 * Info at ExistsErasedAndPureEqualities.fst(68,4-68,11):
   - Admitting continuation.
   - Current context:
@@ -21,9 +19,8 @@
       v#116 : FStar.Ghost.erased Prims.int,
       x#111 : Pulse.Lib.Reference.ref Prims.int
 
->> Got issues: [
-* Error 228 at ExistsErasedAndPureEqualities.fst(79,4-80,21):
+* Info at ExistsErasedAndPureEqualities.fst(79,4-80,21):
+  - Expected failure:
   - Could not resolve all free variables in the proposition: v == v_
   - See also ExistsErasedAndPureEqualities.fst(79,4-81,12)
 
->>]
diff --git a/test/bug-reports/IntroGhost.fst.output.expected b/test/bug-reports/IntroGhost.fst.output.expected
diff --git a/test/bug-reports/PartialApp.fst.output.expected b/test/bug-reports/PartialApp.fst.output.expected
diff --git a/test/nolib/Annots.fst.output.expected b/test/nolib/Annots.fst.output.expected
diff --git a/test/nolib/Bug416.fst.output.expected b/test/nolib/Bug416.fst.output.expected
diff --git a/test/nolib/MatchRange.fst.output.expected b/test/nolib/MatchRange.fst.output.expected
diff --git a/test/nolib/Test.Matcher.fst.output.expected b/test/nolib/Test.Matcher.fst.output.expected
diff --git a/test/nolib/Test.RewriteBy.fst.output.expected b/test/nolib/Test.RewriteBy.fst.output.expected
