1 files changed, 12 insertions, 11 deletions
diff --git a/Test/dafny0/LetExpr.dfy.expect b/Test/dafny0/LetExpr.dfy.expect
index 36fc9361..8f365da3 100644
--- a/Test/dafny0/LetExpr.dfy.expect
+++ b/Test/dafny0/LetExpr.dfy.expect
@@ -1,39 +1,40 @@
-LetExpr.dfy(108,23): Error: assertion violation
+LetExpr.dfy(109,22): Error: assertion violation
 Execution trace:
     (0,0): anon0
     (0,0): anon11_Then
-LetExpr.dfy(8,12): Error: assertion violation
+LetExpr.dfy(9,11): Error: assertion violation
 Execution trace:
     (0,0): anon0
-LetExpr.dfy(253,19): Error: value assigned to a nat must be non-negative
+LetExpr.dfy(254,18): Error: value assigned to a nat must be non-negative
 Execution trace:
     (0,0): anon0
     (0,0): anon5_Then
-LetExpr.dfy(256,19): Error: value assigned to a nat must be non-negative
+LetExpr.dfy(257,18): Error: value assigned to a nat must be non-negative
 Execution trace:
     (0,0): anon0
     (0,0): anon6_Then
-LetExpr.dfy(258,24): Error: value assigned to a nat must be non-negative
+LetExpr.dfy(259,23): Error: value assigned to a nat must be non-negative
 Execution trace:
     (0,0): anon0
     (0,0): anon6_Else
-LetExpr.dfy(287,14): Error: RHS is not certain to look like the pattern 'Agnes'
+LetExpr.dfy(288,13): Error: RHS is not certain to look like the pattern 'Agnes'
 Execution trace:
     (0,0): anon0
     (0,0): anon3_Else
-LetExpr.dfy(304,42): Error: value assigned to a nat must be non-negative
+LetExpr.dfy(305,41): Error: value assigned to a nat must be non-negative
 Execution trace:
     (0,0): anon0
-    (0,0): anon6_Else
-LetExpr.dfy(306,12): Error: assertion violation
+    (0,0): anon7_Else
+LetExpr.dfy(307,11): Error: assertion violation
 Execution trace:
     (0,0): anon0
-    (0,0): anon6_Else
-LetExpr.dfy(316,12): Error: to be compilable, the value of a let-such-that expression must be uniquely determined
+    (0,0): anon7_Else
+LetExpr.dfy(317,11): Error: to be compilable, the value of a let-such-that expression must be uniquely determined
 Execution trace:
     (0,0): anon0
     (0,0): anon10_Then
 
 Dafny program verifier finished with 39 verified, 9 errors
+LetExpr.dfy.tmp.dprint.dfy(162,2): Warning: /!\ No terms found to trigger on.
 
 Dafny program verifier finished with 0 verified, 0 errors