summaryrefslogtreecommitdiff
path: root/Test
diff options
context:
space:
mode:
authorGravatar Bryan Parno <parno@microsoft.com>2014-02-03 22:05:17 -0800
committerGravatar Bryan Parno <parno@microsoft.com>2014-02-03 22:05:17 -0800
commit7885dae08eb13e0fb806989e65b69138cda55001 (patch)
tree0349e9ce031edc43fbfbb5d84666b7a08a836b4c /Test
parent74f1682374a6cee9d837dd773002605a39a84005 (diff)
Provide more detailed feedback for errors involving if-then-else
Diffstat (limited to 'Test')
-rw-r--r--Test/dafny0/Answer4
1 files changed, 2 insertions, 2 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index cd2249c7..b8ebb8e0 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -2073,7 +2073,7 @@ Execution trace:
(0,0): anon0
(0,0): anon9_Then
AutoReq.dfy(36,12): Error: possible violation of function precondition
-AutoReq.dfy(29,6): Related location
+AutoReq.dfy(3,14): Related location
Execution trace:
(0,0): anon0
(0,0): anon9_Then
@@ -2084,7 +2084,7 @@ Execution trace:
(0,0): anon0
(0,0): anon10_Then
AutoReq.dfy(38,12): Error: possible violation of function precondition
-AutoReq.dfy(29,6): Related location
+AutoReq.dfy(3,14): Related location
Execution trace:
(0,0): anon0
(0,0): anon10_Then