Fix issue 121. Don't split QuantifierExpr that are empty.

3 files changed, 23 insertions, 2 deletions

diff --git a/Source/Dafny/Triggers/QuantifierSplitter.cs b/Source/Dafny/Triggers/QuantifierSplitter.cs
index d0b2b430..b039a402 100644
--- a/Source/Dafny/Triggers/QuantifierSplitter.cs
+++ b/Source/Dafny/Triggers/QuantifierSplitter.cs
@@ -100,8 +100,9 @@ namespace Microsoft.Dafny.Triggers {
     }

     

     private static bool AllowsSplitting(QuantifierExpr quantifier) {

-      bool splitAttr = true;

-      return !Attributes.ContainsBool(quantifier.Attributes, "split", ref splitAttr) || splitAttr;

+      // allow split if attributes doesn't contains "split" or it is "split: true" and it is not an empty QuantifierExpr (boundvar.count>0)

+      bool splitAttr = true; 

+      return (!Attributes.ContainsBool(quantifier.Attributes, "split", ref splitAttr) || splitAttr) && (quantifier.BoundVars.Count > 0);

     }

 

     protected override void VisitOneExpr(Expression expr) {

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

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

+

+method Try (a:int, b:int, c:int) 

+{

+	forall

+    ensures a * c == a * c;

+    ensures b * c == b * c;

+	{

+	}

+} 

+

+

+

+

+

+

+

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

+Dafny program verifier finished with 2 verified, 0 errors