diff options
| author |  qunyanm <unknown> | 2015-04-20 13:07:23 -0700 |
|---|---|---|
| committer | qunyanm <unknown> | 2015-04-20 13:07:23 -0700 |
| commit | 9c230b0c9037c30879e865aa5b6d994fee5820ff (patch) | |
| tree | 18346dc55e7170c5b2b1663639adfa3444ab2fc0 /Test/dafny4/Bug73.dfy.expect | |
| parent | d248da33b7763b8c3b2ef75ece9612a45182e7b0 (diff) | |
Fix issue #73. Pass in expr.tok when creating Bpl.Expr for InMap and NotInMap.
Diffstat (limited to 'Test/dafny4/Bug73.dfy.expect')
| -rw-r--r-- | Test/dafny4/Bug73.dfy.expect | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/Test/dafny4/Bug73.dfy.expect b/Test/dafny4/Bug73.dfy.expect new file mode 100644 index 00000000..6cf5c156 --- /dev/null +++ b/Test/dafny4/Bug73.dfy.expect @@ -0,0 +1,12 @@ +Bug73.dfy(7,14): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ Bug73.dfy(7,19): anon3_Else
+ (0,0): anon2
+Bug73.dfy(13,14): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ Bug73.dfy(13,20): anon3_Else
+ (0,0): anon2
+
+Dafny program verifier finished with 2 verified, 2 errors
|