diff --git a/test/MatchBasic.fst.output.expected b/test/MatchBasic.fst.output.expected
index 00cfdcbb6..d88adfa5a 100644
--- a/test/MatchBasic.fst.output.expected
+++ b/test/MatchBasic.fst.output.expected
@@ -1,5 +1,5 @@
->> 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
@@ -7,4 +7,3 @@
   - 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
index 2c2e469e6..bdd618f86 100644
--- 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
index 8743158c1..f52bc0f47 100644
--- 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
index 89a0ae0f9..48ad6064b 100644
--- 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
index fffe4c4c4..4d5e0525d 100644
--- a/test/bug-reports/Bug100.fst.output.expected
+++ b/test/bug-reports/Bug100.fst.output.expected
@@ -1,5 +1,5 @@
->> 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
@@ -7,9 +7,8 @@
     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
@@ -17,9 +16,8 @@
     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
@@ -27,4 +25,3 @@
     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
index 00451263d..cc5325b36 100644
--- 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
index b3cfe018d..c9fdf5947 100644
--- 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
index 113064b2d..6765b7f5d 100644
--- 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
index a3bcf262e..a74b4295d 100644
--- 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
index 289494f9b..2932a4b30 100644
--- 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
index 0622a60b6..9c8ef70c3 100644
--- 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
index b6242e7e5..401159ebd 100644
--- 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
index 5a33352d2..fad0fe5aa 100644
--- 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
index 4c2664c82..dc475d73c 100644
--- 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
index 82e352b9a..ca517e0ba 100644
--- 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
index f7394b6ce..ee2059e7b 100644
--- 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
index 0802a87fd..9a51df501 100644
--- 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
index 6d96bd366..5e5a34c87 100644
--- 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
index 113c50be2..7b405ccae 100644
--- 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
index 3ecf789fd..0e3102487 100644
--- a/test/bug-reports/Bug94.fst.output.expected
+++ b/test/bug-reports/Bug94.fst.output.expected
@@ -1,5 +1,5 @@
->> 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
@@ -7,18 +7,15 @@
     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
index 6f0dba9be..2817eb6ff 100644
--- 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
index b3239a312..3060e70db 100644
--- 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
index c84ae892e..0bf2fd86d 100644
--- a/test/bug-reports/IntroGhost.fst.output.expected
+++ b/test/bug-reports/IntroGhost.fst.output.expected
@@ -1,22 +1,20 @@
->> Got issues: [
-* Error 228 at IntroGhost.fst(44,18-44,20):
+* Info at IntroGhost.fst(44,18-44,20):
+  - Expected failure:
   - Cannot prove:
       Pulse.Lib.Reference.pts_to r ?n
   - In the context:
       IntroGhost.my_inv b r
   - See also IntroGhost.fst(44,9-44,30)
 
->>]
->> Got issues: [
-* Error 228 at IntroGhost.fst(71,2-71,4):
+* Info at IntroGhost.fst(71,2-71,4):
+  - Expected failure:
   - Cannot prove:
       Pulse.Lib.Reference.pts_to r 0
   - In the context:
       IntroGhost.my_inv b r
 
->>]
->> Got issues: [
-* Error 19 at IntroGhost.fst(89,46-92,24):
+* Info at IntroGhost.fst(89,46-92,24):
+  - Expected failure:
   - Failed to discharge match guard for goal:
       IntroGhost.my_inv true r
     with resource from context:
@@ -26,4 +24,3 @@
     details.
   - Also see: IntroGhost.fst(92,17-92,21)
 
->>]
diff --git a/test/bug-reports/PartialApp.fst.output.expected b/test/bug-reports/PartialApp.fst.output.expected
index 2139dd03e..98e297a36 100644
--- a/test/bug-reports/PartialApp.fst.output.expected
+++ b/test/bug-reports/PartialApp.fst.output.expected
@@ -1,11 +1,10 @@
->> Got issues: [
-* Error 228 at PartialApp.fst(26,2-26,3):
+* Info at PartialApp.fst(26,2-26,3):
+  - Expected failure:
   - This statement returns a value of type: Prims.int
   - Did you forget to assign it or ignore it?
 
->>]
->> Got issues: [
-* Error 228 at PartialApp.fst(60,2-60,9):
+* Info at PartialApp.fst(60,2-60,9):
+  - Expected failure:
   - This function is partially applied. Remaining type:
       y: t
         -> Pulse.Lib.Core.stt Prims.unit
@@ -13,4 +12,3 @@
             (fun _ -> Pulse.Lib.Core.emp)
   - Did you forget to apply some arguments?
 
->>]
diff --git a/test/nolib/Annots.fst.output.expected b/test/nolib/Annots.fst.output.expected
index 5638f1b3f..d7d15cc04 100644
--- a/test/nolib/Annots.fst.output.expected
+++ b/test/nolib/Annots.fst.output.expected
@@ -1,40 +1,32 @@
->> Got issues: [
-* Error 168 at Annots.fst(33,2-33,13):
+* Info at Annots.fst(33,2-33,13):
+  - Expected failure:
   - Multiple returns are not allowed.
 
->>]
->> Got issues: [
-* Error 168 at Annots.fst(43,2-43,13):
+* Info at Annots.fst(43,2-43,13):
+  - Expected failure:
   - returns must come before ensures (the name returned is in scope for the ensures clause)
 
->>]
->> Got issues: [
-* Error 168 at Annots.fst(52,2-52,16):
+* Info at Annots.fst(52,2-52,16):
+  - Expected failure:
   - requires must come before any ensures
 
->>]
->> Got issues: [
-* Error 168 at Annots.fst(60,2-60,16):
+* Info at Annots.fst(60,2-60,16):
+  - Expected failure:
   - requires must come before the return
 
->>]
->> Got issues: [
-* Error 168 at Annots.fst(71,2-71,11):
+* Info at Annots.fst(71,2-71,11):
+  - Expected failure:
   - opens must come before the return (the name returned is *not* in scope for the opens clause)
 
->>]
->> Got issues: [
-* Error 168 at Annots.fst(79,2-79,16):
+* Info at Annots.fst(79,2-79,16):
+  - Expected failure:
   - requires must come before any ensures
 
->>]
->> Got issues: [
-* Error 168 at Annots.fst(87,2-87,16):
+* Info at Annots.fst(87,2-87,16):
+  - Expected failure:
   - requires must come before the return
 
->>]
->> Got issues: [
-* Error 72 at Annots.fst(112,15-112,16):
+* Info at Annots.fst(112,15-112,16):
+  - Expected failure:
   - Identifier not found: v
 
->>]
diff --git a/test/nolib/Bug416.fst.output.expected b/test/nolib/Bug416.fst.output.expected
index f76a5737b..fad3e4ce3 100644
--- a/test/nolib/Bug416.fst.output.expected
+++ b/test/nolib/Bug416.fst.output.expected
@@ -1,5 +1,5 @@
->> Got issues: [
-* Error 19 at Bug416.fst(14,19-14,22):
+* Info at Bug416.fst(14,19-14,22):
+  - Expected failure:
   - Ill-typed term: Bug416.foo 2
   - Expected a term of type slprop
   - Assertion failed
@@ -7,4 +7,3 @@
     details.
   - See also Bug416.fst(8,23-8,28)
 
->>]
diff --git a/test/nolib/MatchRange.fst.output.expected b/test/nolib/MatchRange.fst.output.expected
index 411b3bff2..9b405e3e8 100644
--- a/test/nolib/MatchRange.fst.output.expected
+++ b/test/nolib/MatchRange.fst.output.expected
@@ -1,5 +1,5 @@
->> Got issues: [
-* Error 19 at MatchRange.fst(12,2-18,5):
+* Info at MatchRange.fst(12,2-18,5):
+  - 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
@@ -7,9 +7,8 @@
   - Also see: MatchRange.fst(13,6-13,12)
   - Other related locations: dummy(0,0-0,0)
 
->>]
->> Got issues: [
-* Error 19 at MatchRange.fst(28,2-32,3):
+* Info at MatchRange.fst(28,2-32,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
@@ -17,4 +16,3 @@
   - Also see: MatchRange.fst(28,8-28,9)
   - Other related locations: dummy(0,0-0,0)
 
->>]
diff --git a/test/nolib/Test.Matcher.fst.output.expected b/test/nolib/Test.Matcher.fst.output.expected
index ef2101831..ff291bf1a 100644
--- a/test/nolib/Test.Matcher.fst.output.expected
+++ b/test/nolib/Test.Matcher.fst.output.expected
@@ -1,5 +1,5 @@
->> Got issues: [
-* Error 228 at Test.Matcher.fst(69,2-69,4):
+* Info at Test.Matcher.fst(69,2-69,4):
+  - Expected failure:
   - Cannot prove:
       Test.Matcher.fpts_to #Prims.int
         r
@@ -11,4 +11,3 @@
         #(p +. 0.1R)
         (FStar.Ghost.hide #Prims.int 1)
 
->>]
diff --git a/test/nolib/Test.RewriteBy.fst.output.expected b/test/nolib/Test.RewriteBy.fst.output.expected
index 4e4685fdc..423e3f8ee 100644
--- a/test/nolib/Test.RewriteBy.fst.output.expected
+++ b/test/nolib/Test.RewriteBy.fst.output.expected
@@ -1,5 +1,5 @@
->> Got issues: [
-* Error 170 at Test.RewriteBy.fst(31,1-37,8):
+* Info at Test.RewriteBy.fst(31,1-37,8):
+  - Expected failure:
   - rewrite: could not prove equality of
   - Test.RewriteBy.p
   - Test.RewriteBy.q
@@ -14,4 +14,3 @@
           Test.RewriteBy.tac ())
         "(((proofstate)))"
 
->>]