summaryrefslogtreecommitdiff
path: root/Test
diff options
context:
space:
mode:
authorGravatar qunyanm <unknown>2015-11-10 15:53:39 -0800
committerGravatar qunyanm <unknown>2015-11-10 15:53:39 -0800
commit324c2f4bf8842cce7922e7ff7972216dfc06546f (patch)
tree6554d1c5d1fbdab85af2a04e1d44ae709b41ac7f /Test
parent23067608f2d8855abd64982cabfe7f0c7f8e4f5a (diff)
Fix issue 101. Instead of swapping operands for Exp opcode in BinaryExpr,
swap them when the expr is first created in parser or for calcstmt. This avoids problems of operands being swapped again when the expr is copied.
Diffstat (limited to 'Test')
-rw-r--r--Test/dafny4/Bug101.dfy19
-rw-r--r--Test/dafny4/Bug101.dfy.expect8
2 files changed, 27 insertions, 0 deletions
diff --git a/Test/dafny4/Bug101.dfy b/Test/dafny4/Bug101.dfy
new file mode 100644
index 00000000..878ed57a
--- /dev/null
+++ b/Test/dafny4/Bug101.dfy
@@ -0,0 +1,19 @@
+// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+predicate P(i:int) { true }
+
+lemma Tester()
+{
+// forall i ensures false ==> P(i) {}
+ forall i ensures P(i) <== false {}
+ assert forall i :: P(i) ==> false;
+ assert P(0);
+ assert false;
+}
+
+
+
+
+
+
diff --git a/Test/dafny4/Bug101.dfy.expect b/Test/dafny4/Bug101.dfy.expect
new file mode 100644
index 00000000..a4e5f4b3
--- /dev/null
+++ b/Test/dafny4/Bug101.dfy.expect
@@ -0,0 +1,8 @@
+Bug101.dfy(10,11): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon6_Else
+ (0,0): anon7_Then
+ (0,0): anon5
+
+Dafny program verifier finished with 2 verified, 1 error