summaryrefslogtreecommitdiff
path: root/Test/dafny0/Answer
diff options
context:
space:
mode:
authorGravatar rustanleino <unknown>2010-06-09 23:02:36 +0000
committerGravatar rustanleino <unknown>2010-06-09 23:02:36 +0000
commit4d820aa2bcac196188edf21bd52939e1d2031bce (patch)
tree58e6e7e55ca9ca4f2a48944da5b6523a3c2f7baa /Test/dafny0/Answer
parent0f3d7426f849219350c19119a9ecde285df4351b (diff)
Dafny: Another bug fix in SplitExpr, having to do with generic results of function calls
Diffstat (limited to 'Test/dafny0/Answer')
-rw-r--r--Test/dafny0/Answer11
1 files changed, 10 insertions, 1 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 0c152d6e..cc248c20 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -389,8 +389,17 @@ Execution trace:
TypeParameters.dfy(63,27): Error: assertion violation
Execution trace:
(0,0): anon0
+TypeParameters.dfy(130,28): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon5_Then
+TypeParameters.dfy(132,33): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon5_Else
+ (0,0): anon6_Then
-Dafny program verifier finished with 24 verified, 2 errors
+Dafny program verifier finished with 27 verified, 4 errors
-------------------- Datatypes.dfy --------------------