summaryrefslogtreecommitdiff
path: root/Test/hofs/Simple.dfy.expect
diff options
context:
space:
mode:
Diffstat (limited to 'Test/hofs/Simple.dfy.expect')
-rw-r--r--Test/hofs/Simple.dfy.expect12
1 files changed, 6 insertions, 6 deletions
diff --git a/Test/hofs/Simple.dfy.expect b/Test/hofs/Simple.dfy.expect
index e2f16ef3..c0123c80 100644
--- a/Test/hofs/Simple.dfy.expect
+++ b/Test/hofs/Simple.dfy.expect
@@ -1,26 +1,26 @@
-Simple.dfy(14,10): Error: possible division by zero
+Simple.dfy(14,9): Error: possible division by zero
Execution trace:
(0,0): anon0
(0,0): anon6_Else
(0,0): anon7_Then
-Simple.dfy(27,10): Error: possible division by zero
+Simple.dfy(27,9): Error: possible division by zero
Execution trace:
(0,0): anon0
(0,0): anon6_Else
(0,0): anon7_Then
-Simple.dfy(37,9): Error: possible violation of function precondition
+Simple.dfy(37,8): Error: possible violation of function precondition
Execution trace:
(0,0): anon0
Simple.dfy(35,13): anon5_Else
-Simple.dfy(49,9): Error: possible violation of function precondition
+Simple.dfy(49,8): Error: possible violation of function precondition
Execution trace:
(0,0): anon0
(0,0): anon3_Then
(0,0): anon2
-Simple.dfy(61,10): Error: possible violation of function precondition
+Simple.dfy(61,9): Error: possible violation of function precondition
Execution trace:
(0,0): anon0
-Simple.dfy(73,10): Error: assertion violation
+Simple.dfy(73,9): Error: assertion violation
Execution trace:
(0,0): anon0
Simple.dfy(72,38): anon5_Else