Merge

12 files changed, 208 insertions, 53 deletions

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index 9495d64e..4d352f65 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -1335,7 +1335,7 @@ namespace Microsoft.Dafny {
           wr.Write("{0}, ", expr is ForallExpr ? "true" : "false");

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

         }

-        TrExpr(e.Body);

+        TrExpr(e.LogicalBody());

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

           wr.Write(")");

         }

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 39c4c29d..0ce1835f 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -1361,6 +1361,7 @@ QuantifierGuts<out Expression/*!*/ q>
      List<BoundVar/*!*/> bvars = new List<BoundVar/*!*/>();

      Attributes attrs = null;

      Triggers trigs = null;

+     Expression range = null;

      Expression/*!*/ body;

   .)

   ( Forall                                     (. x = t;  univ = true; .)

@@ -1372,12 +1373,15 @@ QuantifierGuts<out Expression/*!*/ q>
     IdentTypeOptional<out bv>                  (. bvars.Add(bv);  parseVarScope.Push(bv.Name, bv.Name); .)

   }

   { AttributeOrTrigger<ref attrs, ref trigs> }

+  [ "|"

+    Expression<out range>

+  ]

   QSep

   Expression<out body>

   (. if (univ) {

-       q = new ForallExpr(x, bvars, body, trigs, attrs);

+       q = new ForallExpr(x, bvars, range, body, trigs, attrs);

      } else {

-       q = new ExistsExpr(x, bvars, body, trigs, attrs);

+       q = new ExistsExpr(x, bvars, range, body, trigs, attrs);

      }

      parseVarScope.PopMarker();

   .)

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index f76f24de..ad7f5fb6 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -2300,17 +2300,23 @@ namespace Microsoft.Dafny {
     }

   }

 

-  public abstract class QuantifierExpr : Expression {

+  /// <summary>

+  /// A ComprehensionExpr has the form:

+  ///   BINDER x Attributes | Range(x) :: Term(x)

+  /// where "Attributes" is optional, and "| Range(x)" is optional and defaults to "true".

+  /// Currently, BINDER is one of the logical quantifiers "exists" or "forall".

+  /// </summary>

+  public abstract class ComprehensionExpr : Expression {

     public readonly List<BoundVar/*!*/>/*!*/ BoundVars;

-    public readonly Expression/*!*/ Body;

+    public readonly Expression Range;

+    public readonly Expression/*!*/ Term;

 

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(BoundVars != null);

-      Contract.Invariant(Body != null);

+      Contract.Invariant(Term != null);

     }

 

-    public readonly Triggers Trigs;

     public readonly Attributes Attributes;

 

     public abstract class BoundedPool { }

@@ -2338,23 +2344,40 @@ namespace Microsoft.Dafny {
     }

 

     public List<BoundedPool> Bounds;  // initialized and filled in by resolver

-    // invariant bounds == null || bounds.Count == BoundVars.Count;

+    // invariant Bounds == null || Bounds.Count == BoundVars.Count;

 

-    public QuantifierExpr(IToken/*!*/ tok, List<BoundVar/*!*/>/*!*/ bvars, Expression/*!*/ body, Triggers trigs, Attributes attrs)

+    public ComprehensionExpr(IToken/*!*/ tok, List<BoundVar/*!*/>/*!*/ bvars, Expression/*!*/ range, Expression/*!*/ term, Attributes attrs)

       : base(tok) {

       Contract.Requires(tok != null);

       Contract.Requires(cce.NonNullElements(bvars));

-      Contract.Requires(body != null);

+      Contract.Requires(term != null);

 

       this.BoundVars = bvars;

-      this.Body = body;

-      this.Trigs = trigs;

+      this.Range = range;

+      this.Term = term;

       this.Attributes = attrs;

     }

 

     public override IEnumerable<Expression> SubExpressions {

-      get { yield return Body; }

+      get {

+        if (Range != null) { yield return Range; }

+        yield return Term; 

+      }

+    }

+  }

+

+  public abstract class QuantifierExpr : ComprehensionExpr {

+    public readonly Triggers Trigs;

+

+    public QuantifierExpr(IToken/*!*/ tok, List<BoundVar/*!*/>/*!*/ bvars, Expression/*!*/ range, Expression/*!*/ term, Triggers trigs, Attributes attrs)

+      : base(tok, bvars, range, term, attrs) {

+      Contract.Requires(tok != null);

+      Contract.Requires(cce.NonNullElements(bvars));

+      Contract.Requires(term != null);

+

+      this.Trigs = trigs;

     }

+    public abstract Expression/*!*/ LogicalBody();

   }

 

   public class Triggers {

@@ -2373,20 +2396,38 @@ namespace Microsoft.Dafny {
   }

 

   public class ForallExpr : QuantifierExpr {

-    public ForallExpr(IToken tok, List<BoundVar/*!*/>/*!*/ bvars, Expression body, Triggers trig, Attributes attrs)

-      : base(tok, bvars, body, trig, attrs) {

+    public ForallExpr(IToken tok, List<BoundVar/*!*/>/*!*/ bvars, Expression range, Expression term, Triggers trig, Attributes attrs)

+      : base(tok, bvars, range, term, trig, attrs) {

       Contract.Requires(cce.NonNullElements(bvars));

       Contract.Requires(tok != null);

-      Contract.Requires(body != null);

+      Contract.Requires(term != null);

+    }

+    public override Expression/*!*/ LogicalBody() {

+      if (Range == null) {

+        return Term;

+      }

+      var body = new BinaryExpr(Term.tok, BinaryExpr.Opcode.Imp, Range, Term);

+      body.ResolvedOp = BinaryExpr.ResolvedOpcode.Imp;

+      body.Type = Term.Type;

+      return body;

     }

   }

 

   public class ExistsExpr : QuantifierExpr {

-    public ExistsExpr(IToken tok, List<BoundVar/*!*/>/*!*/ bvars, Expression body, Triggers trig, Attributes attrs)

-      : base(tok, bvars, body, trig, attrs) {

+    public ExistsExpr(IToken tok, List<BoundVar/*!*/>/*!*/ bvars, Expression range, Expression term, Triggers trig, Attributes attrs)

+      : base(tok, bvars, range, term, trig, attrs) {

       Contract.Requires(cce.NonNullElements(bvars));

       Contract.Requires(tok != null);

-      Contract.Requires(body != null);

+      Contract.Requires(term != null);

+    }

+    public override Expression/*!*/ LogicalBody() {

+      if (Range == null) {

+        return Term;

+      }

+      var body = new BinaryExpr(Term.tok, BinaryExpr.Opcode.And, Range, Term);

+      body.ResolvedOp = BinaryExpr.ResolvedOpcode.And;

+      body.Type = Term.Type;

+      return body;

     }

   }

 

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 70259973..983996d1 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -1920,6 +1920,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		List<BoundVar/*!*/> bvars = new List<BoundVar/*!*/>();

 		Attributes attrs = null;

 		Triggers trigs = null;

+		Expression range = null;

 		Expression/*!*/ body;

 		

 		if (la.kind == 101 || la.kind == 102) {

@@ -1940,12 +1941,16 @@ List<Expression/*!*/>/*!*/ decreases) {
 		while (la.kind == 7) {

 			AttributeOrTrigger(ref attrs, ref trigs);

 		}

+		if (la.kind == 17) {

+			Get();

+			Expression(out range);

+		}

 		QSep();

 		Expression(out body);

 		if (univ) {

-		 q = new ForallExpr(x, bvars, body, trigs, attrs);

+		 q = new ForallExpr(x, bvars, range, body, trigs, attrs);

 		} else {

-		  q = new ExistsExpr(x, bvars, body, trigs, attrs);

+		  q = new ExistsExpr(x, bvars, range, body, trigs, attrs);

 		}

 		parseVarScope.PopMarker();

 		

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 003a977c..6dcf0020 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -931,14 +931,19 @@ namespace Microsoft.Dafny {
         wr.Write(" ");

         PrintAttributes(e.Attributes);

         PrintTriggers(e.Trigs);

+        if (e.Range != null) {

+          wr.Write("| ");

+          PrintExpression(e.Range);

+          wr.Write(" ");

+        }

         wr.Write(":: ");

         if (0 <= indent) {

           int ind = indent + IndentAmount;

           wr.WriteLine();

           Indent(ind);

-          PrintExpression(e.Body, ind);

+          PrintExpression(e.Term, ind);

         } else {

-          PrintExpression(e.Body);

+          PrintExpression(e.Term);

         }

         if (parensNeeded) { wr.Write(")"); }

         

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 6c2f6c38..c7deb42f 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -2227,10 +2227,17 @@ namespace Microsoft.Dafny {
           }

           ResolveType(v.tok, v.Type);

         }

-        ResolveExpression(e.Body, twoState, specContext);

-        Contract.Assert(e.Body.Type != null);  // follows from postcondition of ResolveExpression

-        if (!UnifyTypes(e.Body.Type, Type.Bool)) {

-          Error(expr, "body of quantifier must be of type bool (instead got {0})", e.Body.Type);

+        if (e.Range != null) {

+          ResolveExpression(e.Range, twoState, specContext);

+          Contract.Assert(e.Range.Type != null);  // follows from postcondition of ResolveExpression

+          if (!UnifyTypes(e.Range.Type, Type.Bool)) {

+            Error(expr, "range of quantifier must be of type bool (instead got {0})", e.Range.Type);

+          }

+        }

+        ResolveExpression(e.Term, twoState, specContext);

+        Contract.Assert(e.Term.Type != null);  // follows from postcondition of ResolveExpression

+        if (!UnifyTypes(e.Term.Type, Type.Bool)) {

+          Error(expr, "body of quantifier must be of type bool (instead got {0})", e.Term.Type);

         }

         // Since the body is more likely to infer the types of the bound variables, resolve it

         // first (above) and only then resolve the attributes and triggers (below).

@@ -2391,7 +2398,7 @@ namespace Microsoft.Dafny {
           // Go through the conjuncts of the range expression look for bounds.

           Expression lowerBound = bv.Type is NatType ? new LiteralExpr(bv.tok, new BigInteger(0)) : null;

           Expression upperBound = null;

-          foreach (var conjunct in NormalizedConjuncts(e.Body, e is ExistsExpr)) {

+          foreach (var conjunct in NormalizedConjuncts(e.LogicalBody(), e is ExistsExpr)) {

             var c = conjunct as BinaryExpr;

             if (c == null) {

               goto CHECK_NEXT_CONJUNCT;

@@ -2715,7 +2722,7 @@ namespace Microsoft.Dafny {
 

       } else  if (expr is QuantifierExpr) {

         var e = (QuantifierExpr)expr;

-        var s = FreeVariables(e.Body);

+        var s = FreeVariables(e.LogicalBody());

         foreach (var bv in e.BoundVars) {

           s.Remove(bv);

         }

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 557fcaf0..253a1f9b 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -1511,7 +1511,7 @@ namespace Microsoft.Dafny {
         return z == null ? r : BplAnd(r, z);

       } else if (expr is QuantifierExpr) {

         QuantifierExpr e = (QuantifierExpr)expr;

-        Bpl.Expr total = IsTotal(e.Body, etran);

+        Bpl.Expr total = IsTotal(e.LogicalBody(), etran);

         if (total != Bpl.Expr.True) {

           Bpl.VariableSeq bvars = new Bpl.VariableSeq();

           Bpl.Expr typeAntecedent = etran.TrBoundVariables(e.BoundVars, bvars);

@@ -1638,7 +1638,7 @@ namespace Microsoft.Dafny {
         return BplAnd(t0, t1);

       } else if (expr is QuantifierExpr) {

         QuantifierExpr e = (QuantifierExpr)expr;

-        Bpl.Expr total = CanCallAssumption(e.Body, etran);

+        Bpl.Expr total = CanCallAssumption(e.LogicalBody(), etran);

         if (total != Bpl.Expr.True) {

           Bpl.VariableSeq bvars = new Bpl.VariableSeq();

           Bpl.Expr typeAntecedent = etran.TrBoundVariables(e.BoundVars, bvars);

@@ -1986,7 +1986,7 @@ namespace Microsoft.Dafny {
             builder.Add(new Bpl.AssumeCmd(bv.tok, wh));

           }

         }

-        Expression body = Substitute(e.Body, null, substMap);

+        Expression body = Substitute(e.LogicalBody(), null, substMap);

         CheckWellformed(body, options, locals, builder, etran);

 

       } else if (expr is ITEExpr) {

@@ -4415,13 +4415,17 @@ namespace Microsoft.Dafny {
             }

             tr = new Bpl.Trigger(expr.tok, true, tt, tr);

           }

-          Bpl.Expr body = TrExpr(e.Body);

+          var antecedent = typeAntecedent;

+          if (e.Range != null) {

+            antecedent = Bpl.Expr.And(antecedent, TrExpr(e.Range));

+          }

+          Bpl.Expr body = TrExpr(e.Term);

           

           if (e is ForallExpr) {

-            return new Bpl.ForallExpr(expr.tok, new Bpl.TypeVariableSeq(), bvars, kv, tr, Bpl.Expr.Imp(typeAntecedent, body));

+            return new Bpl.ForallExpr(expr.tok, new Bpl.TypeVariableSeq(), bvars, kv, tr, Bpl.Expr.Imp(antecedent, body));

           } else {

             Contract.Assert(e is ExistsExpr);

-            return new Bpl.ExistsExpr(expr.tok, new Bpl.TypeVariableSeq(), bvars, kv, tr, Bpl.Expr.And(typeAntecedent, body));

+            return new Bpl.ExistsExpr(expr.tok, new Bpl.TypeVariableSeq(), bvars, kv, tr, Bpl.Expr.And(antecedent, body));

           }

         

         } else if (expr is ITEExpr) {

@@ -5220,7 +5224,7 @@ namespace Microsoft.Dafny {
 

             substMap.Add(n, ieK);

           }

-          Expression bodyK = Substitute(e.Body, null, substMap);

+          Expression bodyK = Substitute(e.LogicalBody(), null, substMap);

 

           Bpl.Expr less = DecreasesCheck(toks, types, kk, nn, etran, null, null, false, true);

 

@@ -5252,7 +5256,7 @@ namespace Microsoft.Dafny {
           typeAntecedent = etran.TrBoundVariables(e.BoundVars, bvars);

           foreach (var kase in caseProduct) {

             var ante = BplAnd(BplAnd(typeAntecedent, ih), kase);

-            var bdy = etran.LayerOffset(1).TrExpr(e.Body);

+            var bdy = etran.LayerOffset(1).TrExpr(e.LogicalBody());

             Bpl.Expr q = new Bpl.ForallExpr(kase.tok, bvars, Bpl.Expr.Imp(ante, bdy));

             splits.Add(new SplitExprInfo(false, q));

           }

@@ -5344,7 +5348,7 @@ namespace Microsoft.Dafny {
       // consider automatically applying induction

       var inductionVariables = new List<BoundVar>();

       foreach (var n in e.BoundVars) {

-        if (VarOccursInArgumentToRecursiveFunction(e.Body, n, null)) {

+        if (VarOccursInArgumentToRecursiveFunction(e.LogicalBody(), n, null)) {

           if (CommandLineOptions.Clo.Trace) {

             Console.Write("Applying automatic induction on variable '{0}' of: ", n.Name);

             new Printer(Console.Out).PrintExpression(e);

@@ -5447,7 +5451,7 @@ namespace Microsoft.Dafny {
           VarOccursInArgumentToRecursiveFunction(e.E1, n, p);

       } else if (expr is QuantifierExpr) {

         var e = (QuantifierExpr)expr;

-        return VarOccursInArgumentToRecursiveFunction(e.Body, n, null);

+        return VarOccursInArgumentToRecursiveFunction(e.LogicalBody(), n, null);

       } else if (expr is ITEExpr) {

         var e = (ITEExpr)expr;

         return VarOccursInArgumentToRecursiveFunction(e.Test, n, null) ||  // test is not "elevated"

@@ -5617,14 +5621,15 @@ namespace Microsoft.Dafny {
         

       } else if (expr is QuantifierExpr) {

         QuantifierExpr e = (QuantifierExpr)expr;

-        Expression newBody = Substitute(e.Body, receiverReplacement, substMap);

+        Expression newRange = e.Range == null ? null : Substitute(e.Range, receiverReplacement, substMap);

+        Expression newTerm = Substitute(e.Term, receiverReplacement, substMap);

         Triggers newTrigs = SubstTriggers(e.Trigs, receiverReplacement, substMap);

         Attributes newAttrs = SubstAttributes(e.Attributes, receiverReplacement, substMap);

-        if (newBody != e.Body || newTrigs != e.Trigs || newAttrs != e.Attributes) {

+        if (newRange != e.Range || newTerm != e.Term || newTrigs != e.Trigs || newAttrs != e.Attributes) {

           if (expr is ForallExpr) {

-            newExpr = new ForallExpr(expr.tok, e.BoundVars, newBody, newTrigs, newAttrs);

+            newExpr = new ForallExpr(expr.tok, e.BoundVars, newRange, newTerm, newTrigs, newAttrs);

           } else {

-            newExpr = new ExistsExpr(expr.tok, e.BoundVars, newBody, newTrigs, newAttrs);

+            newExpr = new ExistsExpr(expr.tok, e.BoundVars, newRange, newTerm, newTrigs, newAttrs);

           }

         }

         

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 4bdea760..070aa6be 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -198,8 +198,18 @@ Execution trace:
     (0,0): anon0

     SmallTests.dfy(267,19): anon3_Else

     (0,0): anon2

+SmallTests.dfy(307,3): Error BP5003: A postcondition might not hold on this return path.

+SmallTests.dfy(301,11): Related location: This is the postcondition that might not hold.

+Execution trace:

+    (0,0): anon0

+    (0,0): anon18_Else

+    (0,0): anon11

+    (0,0): anon23_Then

+    (0,0): anon24_Then

+    (0,0): anon15

+    (0,0): anon25_Else

 

-Dafny program verifier finished with 34 verified, 13 errors

+Dafny program verifier finished with 39 verified, 14 errors

 

 -------------------- Definedness.dfy --------------------

 Definedness.dfy(8,7): Error: possible division by zero

@@ -464,14 +474,17 @@ Dafny program verifier finished with 8 verified, 2 errors
 

 -------------------- NonGhostQuantifiers.dfy --------------------

 NonGhostQuantifiers.dfy(13,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'n'

-NonGhostQuantifiers.dfy(57,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'i'

-NonGhostQuantifiers.dfy(61,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'

-NonGhostQuantifiers.dfy(71,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'

-NonGhostQuantifiers.dfy(86,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'

-NonGhostQuantifiers.dfy(94,10): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'y'

-NonGhostQuantifiers.dfy(103,8): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'x'

-NonGhostQuantifiers.dfy(120,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

-8 resolution/type errors detected in NonGhostQuantifiers.dfy

+NonGhostQuantifiers.dfy(42,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'n'

+NonGhostQuantifiers.dfy(46,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'd'

+NonGhostQuantifiers.dfy(50,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'n'

+NonGhostQuantifiers.dfy(74,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'i'

+NonGhostQuantifiers.dfy(78,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'

+NonGhostQuantifiers.dfy(88,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'

+NonGhostQuantifiers.dfy(103,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'

+NonGhostQuantifiers.dfy(111,10): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'y'

+NonGhostQuantifiers.dfy(120,8): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'x'

+NonGhostQuantifiers.dfy(137,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

+11 resolution/type errors detected in NonGhostQuantifiers.dfy

 

 -------------------- AdvancedLHS.dfy --------------------

 AdvancedLHS.dfy(32,23): Error: target object may be null

diff --git a/Test/dafny0/NonGhostQuantifiers.dfy b/Test/dafny0/NonGhostQuantifiers.dfy
index ea256a58..58e64827 100644
--- a/Test/dafny0/NonGhostQuantifiers.dfy
+++ b/Test/dafny0/NonGhostQuantifiers.dfy
@@ -33,6 +33,23 @@ class MyClass<T> {
     (forall n :: 2 <= n ==> 1000 <= n || (exists d :: n < d && d < 2*n))

   }

 

+  function method GoodRange(): bool

+  {

+    (forall n | 2 <= n :: 1000 <= n || (exists d | n < d :: d < 2*n)) && (exists K: nat | K < 100 :: true)

+  }

+  function method BadRangeForall(): bool

+  {

+    forall n | n <= 2 :: 1000 <= n || n % 2 == 0  // error: cannot bound range for n

+  }

+  function method BadRangeExists(): bool

+  {

+    exists d | d < 1000 :: d < 2000  // error: cannot bound range for d

+  }

+  function method WhatAboutThis(): bool

+  {

+    forall n :: 2 <= n && (forall M | M == 1000 :: n < M) ==> n % 2 == 0  // error: heuristics don't get this one for n

+  }

+

   // Here are more tests

 

   function method F(a: array<T>): bool

diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index a839d5a9..ef2049a3 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -272,3 +272,39 @@ class InitCalls {
     r := new InitCalls.InitFromReference(r);  // error, since r.z is unknown

   }

 }

+

+// --------------- some tests with quantifiers and ranges ----------------------

+

+method QuantifierRange0<T>(a: seq<T>, x: T, y: T, N: int)

+  requires 0 <= N && N <= |a|;

+  requires forall k | 0 <= k && k < N :: a[k] != x;

+  requires exists k | 0 <= k && k < N :: a[k] == y;

+  ensures forall k :: 0 <= k && k < N ==> a[k] != x;  // same as the precondition, but using ==> instead of |

+  ensures exists k :: 0 <= k && k < N && a[k] == y;  // same as the precondition, but using && instead of |

+{

+  assert x != y;

+}

+

+method QuantifierRange1<T>(a: seq<T>, x: T, y: T, N: int)

+  requires 0 <= N && N <= |a|;

+  requires forall k :: 0 <= k && k < N ==> a[k] != x;

+  requires exists k :: 0 <= k && k < N && a[k] == y;

+  ensures forall k | 0 <= k && k < N :: a[k] != x;  // same as the precondition, but using | instead of ==>

+  ensures exists k | 0 <= k && k < N :: a[k] == y;  // same as the precondition, but using | instead of &&

+{

+  assert x != y;

+}

+

+method QuantifierRange2<T>(a: seq<T>, x: T, y: T, N: int)

+  requires 0 <= N && N <= |a|;

+  requires exists k | 0 <= k && k < N :: a[k] == y;

+  ensures forall k | 0 <= k && k < N :: a[k] == y;  // error

+{

+  assert N != 0;

+  if (N == 1) {

+    assert forall k | a[if 0 <= k && k < N then k else 0] != y :: k < 0 || N <= k;  // in this case, the precondition holds trivially

+  }

+  if (forall k | 0 <= k && k < N :: a[k] == x) {

+    assert x == y;

+  }

+}

diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer
index d0eba7cb..0111f9af 100644
--- a/Test/dafny1/Answer
+++ b/Test/dafny1/Answer
@@ -65,7 +65,7 @@ Dafny program verifier finished with 4 verified, 0 errors
 

 -------------------- TerminationDemos.dfy --------------------

 

-Dafny program verifier finished with 11 verified, 0 errors

+Dafny program verifier finished with 14 verified, 0 errors

 

 -------------------- Substitution.dfy --------------------

 

diff --git a/Test/dafny1/TerminationDemos.dfy b/Test/dafny1/TerminationDemos.dfy
index 01a7c7bd..49f5a075 100644
--- a/Test/dafny1/TerminationDemos.dfy
+++ b/Test/dafny1/TerminationDemos.dfy
@@ -42,6 +42,28 @@ class Ackermann {
     else

       G(m - 1, G(m, n - 1))

   }

+

+  function H(m: nat, n: nat): nat

+  {

+    if m == 0 then

+      n + 1

+    else if n == 0 then

+      H(m - 1, 1)

+    else

+      H(m - 1, H(m, n - 1))

+  }

+

+  method ComputeAck(m: nat, n: nat) returns (r: nat)

+  {

+    if (m == 0) {

+      r := n + 1;

+    } else if (n == 0) {

+      call r := ComputeAck(m - 1, 1);

+    } else {

+      call s := ComputeAck(m, n - 1);

+      call r := ComputeAck(m - 1, s);

+    }

+  }

 }

 

 // -----------------------------------