Merge

8 files changed, 58 insertions, 15 deletions

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 5fa1085d..ff3b75a3 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -2175,10 +2175,13 @@ ImpliesExpliesExpression<out Expression e0, bool allowSemi, bool allowLambda>
     ( ImpliesOp                                               (. x = t; .)

       ImpliesExpression<out e1, allowSemi, allowLambda>       (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Imp, e0, e1); .)

     | ExpliesOp                                               (. x = t; .)

-      LogicalExpression<out e1, allowSemi, allowLambda>       (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Exp, e0, e1); .)

+      LogicalExpression<out e1, allowSemi, allowLambda>       (. // The order of operands is reversed so that it can be turned into implication during resolution 

+			                                                           e0 = new BinaryExpr(x, BinaryExpr.Opcode.Exp, e1, e0); .)

       { IF(IsExpliesOp())  /* read a reverse implication as far as possible */

         ExpliesOp                                             (. x = t; .)

-        LogicalExpression<out e1, allowSemi, allowLambda>     (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Exp, e0, e1); .)

+        LogicalExpression<out e1, allowSemi, allowLambda>     (. //The order of operands is reversed so that it can be turned into implication during resolution

+				                                                         e0 = new BinaryExpr(x, BinaryExpr.Opcode.Exp, e1, e0); 

+																															.)

       }

     )

   ]

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index fdbd484e..9ed3b7e0 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -4885,7 +4885,12 @@ namespace Microsoft.Dafny {
 

       public override Expression StepExpr(Expression line0, Expression line1)

       {

-        return new BinaryExpr(line0.tok, Op, line0, line1);

+        if (Op == BinaryExpr.Opcode.Exp) {

+          // The order of operands is reversed so that it can be turned into implication during resolution 

+          return new BinaryExpr(line0.tok, Op, line1, line0);

+        } else {

+          return new BinaryExpr(line0.tok, Op, line0, line1);

+        }

       }

 

       public override string ToString()

@@ -6779,14 +6784,8 @@ namespace Microsoft.Dafny {
       Contract.Requires(e0 != null);

       Contract.Requires(e1 != null);

       this.Op = op;

-      if (op == Opcode.Exp) {

-        // The order of operands is reversed so that it can be turned into implication during resolution

-        this.E0 = e1;

-        this.E1 = e0;

-      } else {

-        this.E0 = e0;

-        this.E1 = e1;

-      }

+      this.E0 = e0;

+      this.E1 = e1;

     }

 

     /// <summary>

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 6a5f32ab..b6a59f4e 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -3267,12 +3267,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				ExpliesOp();

 				x = t; 

 				LogicalExpression(out e1, allowSemi, allowLambda);

-				e0 = new BinaryExpr(x, BinaryExpr.Opcode.Exp, e0, e1); 

+				e0 = new BinaryExpr(x, BinaryExpr.Opcode.Exp, e1, e0); 

 				while (IsExpliesOp()) {

 					ExpliesOp();

 					x = t; 

 					LogicalExpression(out e1, allowSemi, allowLambda);

-					e0 = new BinaryExpr(x, BinaryExpr.Opcode.Exp, e0, e1); 

+					e0 = new BinaryExpr(x, BinaryExpr.Opcode.Exp, e1, e0); 

+					

 				}

 			} else SynErr(219);

 		}

diff --git a/Source/Dafny/Triggers/TriggersCollector.cs b/Source/Dafny/Triggers/TriggersCollector.cs
index c25f65b9..698ea3b5 100644
--- a/Source/Dafny/Triggers/TriggersCollector.cs
+++ b/Source/Dafny/Triggers/TriggersCollector.cs
@@ -201,8 +201,8 @@ namespace Microsoft.Dafny.Triggers {
           (expr is UnaryOpExpr && (((UnaryOpExpr)expr).Op == UnaryOpExpr.Opcode.Cardinality)) || // FIXME || ((UnaryOpExpr)expr).Op == UnaryOpExpr.Opcode.Fresh doesn't work, as fresh is a pretty tricky predicate when it's not about datatypes. See translator.cs:10944

           (expr is BinaryExpr && (((BinaryExpr)expr).Op == BinaryExpr.Opcode.NotIn || ((BinaryExpr)expr).Op == BinaryExpr.Opcode.In))) {

         annotation = AnnotatePotentialCandidate(expr);

-      } else if (expr is QuantifierExpr && ((QuantifierExpr)expr).SplitQuantifier == null) {

-        annotation = AnnotateQuantifier((QuantifierExpr)expr);

+      } else if (expr is QuantifierExpr) {

+          annotation = AnnotateQuantifier((QuantifierExpr)expr);

       } else if (expr is LetExpr) {

         annotation = AnnotateLetExpr((LetExpr)expr);

       } else if (expr is IdentifierExpr) {

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

diff --git a/Test/dafny4/Bug99.dfy b/Test/dafny4/Bug99.dfy
new file mode 100644
index 00000000..3f95ce9f
--- /dev/null
+++ b/Test/dafny4/Bug99.dfy
@@ -0,0 +1,11 @@
+// RUN: %dafny  /autoTriggers:1 /compile:0 "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+predicate P(e:int, p:int) { true }

+predicate Q(i:int, t:int)

+

+lemma Tester(x:int)

+{

+    assert forall i :: Q(i, x) ==> (forall p {:trigger P(i, p)} :: P(i, p));

+		

+}

diff --git a/Test/dafny4/Bug99.dfy.expect b/Test/dafny4/Bug99.dfy.expect
new file mode 100644
index 00000000..73ba063c
--- /dev/null
+++ b/Test/dafny4/Bug99.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 4 verified, 0 errors