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 | |
| parent | d248da33b7763b8c3b2ef75ece9612a45182e7b0 (diff) | |
Fix issue #73. Pass in expr.tok when creating Bpl.Expr for InMap and NotInMap.
Diffstat (limited to 'Test/dafny4')
| -rw-r--r-- | Test/dafny4/Bug73.dfy | 14 | ||||
| -rw-r--r-- | Test/dafny4/Bug73.dfy.expect | 12 |
2 files changed, 26 insertions, 0 deletions
diff --git a/Test/dafny4/Bug73.dfy b/Test/dafny4/Bug73.dfy new file mode 100644 index 00000000..c21f818a --- /dev/null +++ b/Test/dafny4/Bug73.dfy @@ -0,0 +1,14 @@ +// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+lemma L(m:map<int, int>, r:int, i:int)
+ requires i != r;
+{
+ assert i in m && i != r;
+}
+
+lemma L2(m:map<int, int>, r:int, i:int)
+ requires i != r;
+{
+ assert i !in m && i != r;
+}
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
|