From 324c2f4bf8842cce7922e7ff7972216dfc06546f Mon Sep 17 00:00:00 2001
From: qunyanm <unknown>
Date: Tue, 10 Nov 2015 15:53:39 -0800
Subject: 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.

---
 Test/dafny4/Bug101.dfy | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)
 create mode 100644 Test/dafny4/Bug101.dfy

(limited to 'Test/dafny4/Bug101.dfy')

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;
+}
+
+
+
+
+
+
-- 
cgit v1.2.3