summaryrefslogtreecommitdiff
path: root/Test/dafny0/Basics.dfy.expect
diff options
context:
space:
mode:
Diffstat (limited to 'Test/dafny0/Basics.dfy.expect')
-rw-r--r--Test/dafny0/Basics.dfy.expect36
1 files changed, 18 insertions, 18 deletions
diff --git a/Test/dafny0/Basics.dfy.expect b/Test/dafny0/Basics.dfy.expect
index f28df20a..65d5d101 100644
--- a/Test/dafny0/Basics.dfy.expect
+++ b/Test/dafny0/Basics.dfy.expect
@@ -1,8 +1,8 @@
-Basics.dfy(45,14): Error: assertion violation
+Basics.dfy(45,13): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon3_Else
-Basics.dfy(69,42): Error: assertion violation
+Basics.dfy(69,41): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon13_Then
@@ -12,7 +12,7 @@ Execution trace:
Basics.dfy(69,82): anon17_Else
Basics.dfy(69,95): anon18_Else
(0,0): anon12
-Basics.dfy(93,14): Error: assertion violation
+Basics.dfy(93,13): Error: assertion violation
Execution trace:
(0,0): anon0
Basics.dfy(83,14): anon27_Else
@@ -27,7 +27,7 @@ Execution trace:
Basics.dfy(91,13): anon34_Else
(0,0): anon35_Then
(0,0): anon15
-Basics.dfy(99,14): Error: assertion violation
+Basics.dfy(99,13): Error: assertion violation
Execution trace:
(0,0): anon0
Basics.dfy(83,14): anon27_Else
@@ -42,7 +42,7 @@ Execution trace:
Basics.dfy(97,19): anon40_Else
(0,0): anon41_Then
(0,0): anon26
-Basics.dfy(112,28): Error: target object may be null
+Basics.dfy(112,27): Error: target object may be null
Execution trace:
(0,0): anon0
Basics.dfy(105,20): anon13_Else
@@ -52,7 +52,7 @@ Execution trace:
Basics.dfy(107,24): anon15_Else
(0,0): anon6
(0,0): anon16_Then
-Basics.dfy(114,14): Error: target object may be null
+Basics.dfy(114,13): Error: target object may be null
Execution trace:
(0,0): anon0
Basics.dfy(105,20): anon13_Else
@@ -62,11 +62,11 @@ Execution trace:
Basics.dfy(107,24): anon15_Else
(0,0): anon6
(0,0): anon16_Else
-Basics.dfy(149,16): Error: assertion violation
+Basics.dfy(149,15): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon10_Then
-Basics.dfy(168,10): Error: when left-hand sides 0 and 1 may refer to the same location, they must be assigned the same value
+Basics.dfy(168,9): Error: when left-hand sides 0 and 1 may refer to the same location, they must be assigned the same value
Execution trace:
(0,0): anon0
(0,0): anon10_Then
@@ -75,28 +75,28 @@ Execution trace:
(0,0): anon6
(0,0): anon12_Then
(0,0): anon9
-Basics.dfy(182,10): Error: when left-hand sides 0 and 1 refer to the same location, they must be assigned the same value
+Basics.dfy(182,9): Error: when left-hand sides 0 and 1 refer to the same location, they must be assigned the same value
Execution trace:
(0,0): anon0
-Basics.dfy(194,19): Error: assertion violation
+Basics.dfy(194,18): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon11_Then
-Basics.dfy(196,10): Error: assignment may update an object not in the enclosing context's modifies clause
+Basics.dfy(196,9): Error: assignment may update an object not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
(0,0): anon3
-Basics.dfy(196,10): Error: target object may be null
+Basics.dfy(196,9): Error: target object may be null
Execution trace:
(0,0): anon0
(0,0): anon3
-Basics.dfy(201,12): Error: left-hand sides 0 and 1 may refer to the same location
+Basics.dfy(201,11): Error: left-hand sides 0 and 1 may refer to the same location
Execution trace:
(0,0): anon0
(0,0): anon11_Then
(0,0): anon3
(0,0): anon12_Then
-Basics.dfy(212,15): Error: assertion violation
+Basics.dfy(212,14): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon11_Then
@@ -106,19 +106,19 @@ Execution trace:
(0,0): anon13_Then
(0,0): anon8
(0,0): anon14_Then
-Basics.dfy(274,10): Error: when left-hand sides 0 and 1 refer to the same location, they must be assigned the same value
+Basics.dfy(274,9): Error: when left-hand sides 0 and 1 refer to the same location, they must be assigned the same value
Execution trace:
(0,0): anon0
-Basics.dfy(465,12): Error: assertion violation
+Basics.dfy(465,11): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon4_Then
(0,0): anon3
-Basics.dfy(476,19): Error: assertion violation
+Basics.dfy(476,18): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon4_Else
-Basics.dfy(478,12): Error: assertion violation
+Basics.dfy(478,11): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon4_Then