Update expected error output

mtzguido · mtzguido · commit c54e5444d3e4 · 2025-10-26T17:42:39.000-07:00
diff --git a/test/LoopInvariants.fst.output.expected b/test/LoopInvariants.fst.output.expected
@@ -2,7 +2,7 @@
   - Expected failure:
   - When using multiple invariants, they must all be in the "new" style without a binder.
 
-* Info at LoopInvariants.fst(76,20-77,10):
+* Info at LoopInvariants.fst(77,9-77,10):
   - Expected failure:
   - rewrite: could not prove equality of
   - Pulse.Lib.Reference.pts_to s 3
@@ -11,7 +11,7 @@
   - The SMT solver could not prove the query. Use --query_stats for more
     details.
 
-* Info at LoopInvariants.fst(83,18-88,10):
+* Info at LoopInvariants.fst(88,9-88,10):
   - Expected failure:
   - rewrite: could not prove equality of
   - Pulse.Lib.Reference.pts_to s 3
diff --git a/test/MatchBasic.fst.output.expected b/test/MatchBasic.fst.output.expected
@@ -1,4 +1,4 @@
-* Info at MatchBasic.fst(149,0-157,1):
+* Info at MatchBasic.fst(154,2-156,3):
   - Expected failure:
   - Could not verify that this match is exhaustive.
   - Patterns are incomplete
diff --git a/test/Test.Recursion.fst.output.expected b/test/Test.Recursion.fst.output.expected
@@ -1,4 +1,4 @@
-* Info at Test.Recursion.fst(92,12-92,14):
+* Info at Test.Recursion.fst(94,2-94,20):
   - Expected failure:
   - Ill-typed term: test_ghost_loop ()
   - Expected a term of type
@@ -10,7 +10,7 @@
   - The SMT solver could not prove the query. Use --query_stats for more
     details.
 
-* Info at Test.Recursion.fst(138,12-138,13):
+* Info at Test.Recursion.fst(141,4-141,22):
   - Expected failure:
   - Ill-typed term: test5' (z - 1) (y - 1)
   - Expected a term of type
diff --git a/test/bug-reports/Bug.DesugaringError.fst.output.expected b/test/bug-reports/Bug.DesugaringError.fst.output.expected
@@ -10,6 +10,7 @@
 * 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)
 
 * Info at Bug.DesugaringError.fst(46,4-46,8):
   - Expected failure:
diff --git a/test/bug-reports/Bug.SpinLock.fst.output.expected b/test/bug-reports/Bug.SpinLock.fst.output.expected
@@ -1,4 +1,4 @@
-* Info at Bug.SpinLock.fst(39,0-46,1):
+* Info at Bug.SpinLock.fst(45,2-45,4):
   - Expected failure:
   - Tactic failed
   - Cannot prove:
diff --git a/test/bug-reports/Bug111.fst.output.expected b/test/bug-reports/Bug111.fst.output.expected
@@ -1,4 +1,4 @@
-* Info at Bug111.fst(7,0-21,1):
+* 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/Bug174.fst.output.expected b/test/bug-reports/Bug174.fst.output.expected
@@ -1,4 +1,4 @@
-* Info at Bug174.fst(11,11-13,41):
+* Info at Bug174.fst(15,1-17,10):
   - Expected failure:
   - rewrite: could not prove equality of
   - Pulse.Lib.Reference.pts_to r v
diff --git a/test/bug-reports/Bug206.fst.output.expected b/test/bug-reports/Bug206.fst.output.expected
@@ -8,5 +8,5 @@
   - Assertion failed
   - The SMT solver could not prove the query. Use --query_stats for more
     details.
-  - See also Bug206.fst(6,20-6,20)
+  - See also Bug206.fst(18,2-18,8)
 
diff --git a/test/bug-reports/Bug267.fst.output.expected b/test/bug-reports/Bug267.fst.output.expected
@@ -11,7 +11,7 @@
   - The SMT solver could not prove the query. Use --query_stats for more
     details.
   - Also see: Prims.fst(161,28-183,79)
-  - See also Bug267.fst(43,18-43,21)
+  - See also Bug267.fst(61,4-61,8)
 
 * Info at Bug267.fst(65,53-66,17):
   - Expected failure:
diff --git a/test/bug-reports/Bug278.fst.output.expected b/test/bug-reports/Bug278.fst.output.expected
@@ -1,4 +1,4 @@
-* Info at Bug278.fst(31,0-38,1):
+* Info at Bug278.fst(35,5-37,5):
   - Expected failure:
   - Tactic failed
   - Internal error: unexpected unresolved (universe) uvar in deep_compress: 21
diff --git a/test/bug-reports/Bug36.fst.output.expected b/test/bug-reports/Bug36.fst.output.expected
@@ -1,4 +1,5 @@
 * 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,4 +1,4 @@
-* Info at Bug45.fst(54,0-68,1):
+* Info at Bug45.fst(61,10-66,5):
   - Expected failure:
   - Tactic failed
   - Internal error: unexpected unresolved (universe) uvar in deep_compress: 75
diff --git a/test/bug-reports/Bug59.fst.output.expected b/test/bug-reports/Bug59.fst.output.expected
@@ -1,4 +1,4 @@
-* Info at Bug59.fst(11,30-11,37):
+* Info at Bug59.fst(12,11-12,24):
   - Expected failure:
   - Ill-typed term: pure (x == y)
   - Expected a term of type slprop
diff --git a/test/bug-reports/Bug94.fst.output.expected b/test/bug-reports/Bug94.fst.output.expected
@@ -10,12 +10,12 @@
 * 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)
 
-* Info at Bug94.fst(34,18-34,24):
+* 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.
-  - See also Bug94.fst(26,19-26,32)
 
diff --git a/test/bug-reports/ExistsErasedAndPureEqualities.fst.output.expected b/test/bug-reports/ExistsErasedAndPureEqualities.fst.output.expected
@@ -9,7 +9,7 @@
       v#267 : FStar.Ghost.erased Prims.int,
       x#262 : Pulse.Lib.Reference.ref Prims.int
 
-* Info at ExistsErasedAndPureEqualities.fst(67,0-76,1):
+* Info at ExistsErasedAndPureEqualities.fst(71,4-73,12):
   - Expected failure:
   - Ill-typed term: pure (v == (*?u106*)_)
   - Expected a term of type slprop
diff --git a/test/bug-reports/IntroGhost.fst.output.expected b/test/bug-reports/IntroGhost.fst.output.expected
@@ -6,7 +6,7 @@
   - In the context:
       IntroGhost.my_inv _b2 r
 
-* Info at IntroGhost.fst(61,0-72,1):
+* Info at IntroGhost.fst(71,2-71,4):
   - Expected failure:
   - Tactic failed
   - Cannot prove:
diff --git a/test/nolib/ErrCantFindWitness.fst.output.expected b/test/nolib/ErrCantFindWitness.fst.output.expected
@@ -1,4 +1,4 @@
-* Info at ErrCantFindWitness.fst(6,0-8,2):
+* Info at ErrCantFindWitness.fst(8,1-8,1):
   - Expected failure:
   - Cannot find witness for (exists* (x:Prims.nat). emp)
   - Ill-typed term: (*?u56*)_
diff --git a/test/nolib/MatchRange.fst.output.expected b/test/nolib/MatchRange.fst.output.expected
@@ -1,4 +1,4 @@
-* Info at MatchRange.fst(7,0-19,1):
+* Info at MatchRange.fst(12,2-18,5):
   - Expected failure:
   - Could not verify that this match is exhaustive.
   - Patterns are incomplete
@@ -7,7 +7,7 @@
   - Also see: MatchRange.fst(13,6-13,12)
   - Other related locations: dummy(0,0-0,0)
 
-* Info at MatchRange.fst(22,0-33,1):
+* Info at MatchRange.fst(28,2-32,3):
   - Expected failure:
   - Could not verify that this match is exhaustive.
   - Patterns are incomplete
diff --git a/test/nolib/Test.Matcher.fst.output.expected b/test/nolib/Test.Matcher.fst.output.expected
@@ -1,4 +1,4 @@
-* Info at Test.Matcher.fst(66,0-69,7):
+* Info at Test.Matcher.fst(69,2-69,4):
   - Expected failure:
   - Tactic failed
   - Cannot prove:
diff --git a/test/nolib/Test.RewriteBy.fst.output.expected b/test/nolib/Test.RewriteBy.fst.output.expected
@@ -1,4 +1,4 @@
-* Info at Test.RewriteBy.fst(28,0-38,1):
+* Info at Test.RewriteBy.fst(31,1-37,8):
   - Expected failure:
   - rewrite: could not prove equality of
   - Test.RewriteBy.p

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-* Info at MatchBasic.fst(149,0-157,1):`
	`1`	`+* Info at MatchBasic.fst(154,2-156,3):`
`2`	`2`	`- Expected failure:`
`3`	`3`	`- Could not verify that this match is exhaustive.`
`4`	`4`	`- Patterns are incomplete`
Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-* Info at Bug.SpinLock.fst(39,0-46,1):`
	`1`	`+* Info at Bug.SpinLock.fst(45,2-45,4):`
`2`	`2`	`- Expected failure:`
`3`	`3`	`- Tactic failed`
`4`	`4`	`- Cannot prove:`
Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-* Info at Bug111.fst(7,0-21,1):`
	`1`	`+* Info at Bug111.fst(13,2-20,3):`
`2`	`2`	`- Expected failure:`
`3`	`3`	`- Could not verify that this match is exhaustive.`
`4`	`4`	`- Type of pattern (Prims.int) does not match type of scrutinee (FStar.Ghost.erased Prims.int)`
Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-* Info at Bug174.fst(11,11-13,41):`
	`1`	`+* Info at Bug174.fst(15,1-17,10):`
`2`	`2`	`- Expected failure:`
`3`	`3`	`- rewrite: could not prove equality of`
`4`	`4`	`- Pulse.Lib.Reference.pts_to r v`
Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-* Info at Bug278.fst(31,0-38,1):`
	`1`	`+* Info at Bug278.fst(35,5-37,5):`
`2`	`2`	`- Expected failure:`
`3`	`3`	`- Tactic failed`
`4`	`4`	`- Internal error: unexpected unresolved (universe) uvar in deep_compress: 21`