Merge

1 files changed, 4 insertions, 1 deletions

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index 619638ac..f2cc5d23 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -2810,6 +2810,9 @@ namespace Microsoft.Dafny {
 

       } else if (expr is QuantifierExpr) {

         var e = (QuantifierExpr)expr;

+

+        // Compilation does not check whether a quantifier was split.

+        

         Contract.Assert(e.Bounds != null);  // for non-ghost quantifiers, the resolver would have insisted on finding bounds

         var n = e.BoundVars.Count;

         Contract.Assert(e.Bounds.Count == n);

@@ -2852,7 +2855,7 @@ namespace Microsoft.Dafny {
           wr.Write("{0}, ", expr is ForallExpr ? "true" : "false");

           wr.Write("@{0} => ", bv.CompileName);

         }

-        TrExpr(e.LogicalBody());

+        TrExpr(e.LogicalBody(true));

         for (int i = 0; i < n; i++) {

           wr.Write(")");

         }