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.

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