summaryrefslogtreecommitdiff
path: root/Test/dafny0/Modules1.dfy.expect
diff options
context:
space:
mode:
Diffstat (limited to 'Test/dafny0/Modules1.dfy.expect')
-rw-r--r--Test/dafny0/Modules1.dfy.expect12
1 files changed, 6 insertions, 6 deletions
diff --git a/Test/dafny0/Modules1.dfy.expect b/Test/dafny0/Modules1.dfy.expect
index 342b5808..feddf46a 100644
--- a/Test/dafny0/Modules1.dfy.expect
+++ b/Test/dafny0/Modules1.dfy.expect
@@ -1,20 +1,20 @@
-Modules1.dfy(79,16): Error: assertion violation
+Modules1.dfy(79,15): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-Modules1.dfy(92,16): Error: assertion violation
+Modules1.dfy(92,15): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-Modules1.dfy(94,18): Error: assertion violation
+Modules1.dfy(94,17): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon3_Else
-Modules1.dfy(56,9): Error: decreases expression must be bounded below by 0
-Modules1.dfy(54,13): Related location
+Modules1.dfy(56,8): Error: decreases expression must be bounded below by 0
+Modules1.dfy(54,12): Related location
Execution trace:
(0,0): anon0
-Modules1.dfy(62,9): Error: failure to decrease termination measure
+Modules1.dfy(62,8): Error: failure to decrease termination measure
Execution trace:
(0,0): anon0