summaryrefslogtreecommitdiff
path: root/Test/dafny0/Parallel.dfy.expect
diff options
context:
space:
mode:
authorGravatar leino <unknown>2014-12-02 14:04:53 -0800
committerGravatar leino <unknown>2014-12-02 14:04:53 -0800
commit682a34e72274aff3ef4ebcbe54244d1c2ca0ba2f (patch)
tree448289d84b91a081f7658710f0fcb9cc425805c8 /Test/dafny0/Parallel.dfy.expect
parentd5685d5afcd053a0bb2178425e1b1d12cd85eb52 (diff)
Snapshot, to be continued
Diffstat (limited to 'Test/dafny0/Parallel.dfy.expect')
-rw-r--r--Test/dafny0/Parallel.dfy.expect4
1 files changed, 2 insertions, 2 deletions
diff --git a/Test/dafny0/Parallel.dfy.expect b/Test/dafny0/Parallel.dfy.expect
index c994cd39..6b726cd5 100644
--- a/Test/dafny0/Parallel.dfy.expect
+++ b/Test/dafny0/Parallel.dfy.expect
@@ -1,4 +1,4 @@
-Parallel.dfy(34,5): Error BP5002: A precondition for this call might not hold.
+Parallel.dfy(34,10): Error BP5002: A precondition for this call might not hold.
Parallel.dfy(60,14): Related location: This is the precondition that might not hold.
Execution trace:
(0,0): anon0
@@ -60,7 +60,7 @@ Execution trace:
(0,0): anon19_Then
(0,0): anon20_Then
(0,0): anon5
-Parallel.dfy(296,10): Error: assertion violation
+Parallel.dfy(296,20): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon4_Else