Beefed up assign/let-such-that to generate possible witnesses for set/multiset/sequence/map display expressions

Run SmallTests.dfy and LetExpr.dfy only once in the test suite
Fixed some translation bugs (and a pretty-printing bug) for map display expressions

6 files changed, 148 insertions, 263 deletions

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index e6fe3468..930af474 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -1025,9 +1025,9 @@ namespace Microsoft.Dafny {
       } else if (expr is MapDisplayExpr) {

         MapDisplayExpr e = (MapDisplayExpr)expr;

         wr.Write("map");

-        wr.Write("{");

+        wr.Write("[");

         PrintExpressionPairList(e.Elements);

-        wr.Write("}");

+        wr.Write("]");

       } else if (expr is ExprDotName) {

         var e = (ExprDotName)expr;

         // determine if parens are needed

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 5219be3f..efadc090 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -6315,13 +6315,15 @@ namespace Microsoft.Dafny
         if (bv.Type is BoolType) {

           // easy

           bounds.Add(new ComprehensionExpr.BoolBoundedPool());

-        } else if (bv.Type.IsIndDatatype && (bv.Type.AsIndDatatype).HasFinitePossibleValues) {

-          bounds.Add(new ComprehensionExpr.DatatypeBoundedPool(bv.Type.AsIndDatatype));

         } else {

+          bool foundBoundsForBv = false;

+          if (bv.Type.IsIndDatatype && (bv.Type.AsIndDatatype).HasFinitePossibleValues) {

+            bounds.Add(new ComprehensionExpr.DatatypeBoundedPool(bv.Type.AsIndDatatype));

+            foundBoundsForBv = true;

+          }

           // Go through the conjuncts of the range expression to look for bounds.

           Expression lowerBound = bv.Type is NatType ? Resolver.CreateResolvedLiteral(bv.tok, 0) : null;

           Expression upperBound = null;

-          bool foundBoundsForBv = false;

           if (returnAllBounds && lowerBound != null) {

             bounds.Add(new ComprehensionExpr.IntBoundedPool(lowerBound, upperBound));

             lowerBound = null;

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 3d4e8a98..2feedc01 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -5066,7 +5066,6 @@ namespace Microsoft.Dafny {
     IEnumerable<Expression> GuessWitnesses(BoundVar x, Expression expr) {

       Contract.Requires(x != null);

       Contract.Requires(expr != null);

-      var lookForBounds = false;

       if (x.Type is BoolType) {

         var lit = new LiteralExpr(x.tok, false);

         lit.Type = Type.Bool;  // resolve here

@@ -5074,49 +5073,74 @@ namespace Microsoft.Dafny {
         lit = new LiteralExpr(x.tok, true);

         lit.Type = Type.Bool;  // resolve here

         yield return lit;

+        yield break;  // there are no more possible witnesses for booleans

       } else if (x.Type.IsRefType) {

-        var lit = new LiteralExpr(x.tok);

+        var lit = new LiteralExpr(x.tok);  // null

         lit.Type = x.Type;

         yield return lit;

-      } else if (x.Type.IsIndDatatype) {

-        var dt = x.Type.AsIndDatatype;

+      } else if (x.Type.IsDatatype) {

+        var dt = x.Type.AsDatatype;

         Expression zero = Zero(x.tok, x.Type);

         if (zero != null) {

           yield return zero;

         }

+        foreach (var ctor in dt.Ctors) {

+          if (ctor.Formals.Count == 0) {

+            var v = new DatatypeValue(x.tok, dt.Name, ctor.Name, new List<Expression>());

+            v.Ctor = ctor;  // resolve here

+            v.Type = new UserDefinedType(x.tok, dt.Name, dt, new List<Type>());  // resolve here

+            yield return v;

+          }

+        }

       } else if (x.Type is SetType) {

         var empty = new SetDisplayExpr(x.tok, new List<Expression>());

         empty.Type = x.Type;

         yield return empty;

-        lookForBounds = true;

       } else if (x.Type is MultiSetType) {

         var empty = new MultiSetDisplayExpr(x.tok, new List<Expression>());

         empty.Type = x.Type;

         yield return empty;

-        lookForBounds = true;

       } else if (x.Type is SeqType) {

         var empty = new SeqDisplayExpr(x.tok, new List<Expression>());

         empty.Type = x.Type;

         yield return empty;

-        lookForBounds = true;

       } else if (x.Type is IntType) {

         var lit = new LiteralExpr(x.tok, 0);

         lit.Type = Type.Int;  // resolve here

         yield return lit;

-        lookForBounds = true;

-      }

-      if (lookForBounds) {

-        var missingBounds = new List<BoundVar>();

-        var bounds = Resolver.DiscoverBounds(x.tok, new List<BoundVar>() { x }, expr, true, true, missingBounds);

-        if (missingBounds.Count == 0) {

-          foreach (var bound in bounds) {

-            if (bound is ComprehensionExpr.IntBoundedPool) {

-              var bnd = (ComprehensionExpr.IntBoundedPool)bound;

-              if (bnd.LowerBound != null) yield return bnd.LowerBound;

-              if (bnd.UpperBound != null) yield return Resolver.Minus(bnd.UpperBound, 1);

-            } else if (bound is ComprehensionExpr.SuperSetBoundedPool) {

-              var bnd = (ComprehensionExpr.SuperSetBoundedPool)bound;

-              yield return bnd.LowerBound;

+      }

+

+      var missingBounds = new List<BoundVar>();

+      var bounds = Resolver.DiscoverBounds(x.tok, new List<BoundVar>() { x }, expr, true, true, missingBounds);

+      if (missingBounds.Count == 0) {

+        foreach (var bound in bounds) {

+          if (bound is ComprehensionExpr.IntBoundedPool) {

+            var bnd = (ComprehensionExpr.IntBoundedPool)bound;

+            if (bnd.LowerBound != null) yield return bnd.LowerBound;

+            if (bnd.UpperBound != null) yield return Resolver.Minus(bnd.UpperBound, 1);

+          } else if (bound is ComprehensionExpr.SuperSetBoundedPool) {

+            var bnd = (ComprehensionExpr.SuperSetBoundedPool)bound;

+            yield return bnd.LowerBound;

+          } else if (bound is ComprehensionExpr.SetBoundedPool) {

+            var st = ((ComprehensionExpr.SetBoundedPool)bound).Set.Resolved;

+            if (st is DisplayExpression) {

+              var display = (DisplayExpression)st;

+              foreach (var el in display.Elements) {

+                yield return el;

+              }

+            } else if (st is MapDisplayExpr) {

+              var display = (MapDisplayExpr)st;

+              foreach (var maplet in display.Elements) {

+                yield return maplet.A;

+              }

+            }

+          } else if (bound is ComprehensionExpr.SeqBoundedPool) {

+            var sq = ((ComprehensionExpr.SeqBoundedPool)bound).Seq.Resolved;

+            var display = sq as DisplayExpression;

+            if (display != null) {

+              foreach (var el in display.Elements) {

+                yield return el;

+              }

             }

           }

         }

@@ -6442,28 +6466,28 @@ namespace Microsoft.Dafny {
         MapType mt = (MapType)type;

         Bpl.Type maptype = predef.MapType(tok, predef.BoxType, predef.BoxType);

         Bpl.Expr clause = null;

-        // (forall i: BoxType :: { Map#Domain(x)[i] }

-        //      Map#Domain(x)[i] ==> Unbox(i)-has-the-expected-type)

-        // (forall i: BoxType :: { Map#Elements(x)[i] }

-        //      Map#Domain(x)[i] ==> Unbox(Map#Elements(x)[i])-has-the-expected-type)

+        // (forall t: BoxType :: { Map#Domain(x)[t] }

+        //      Map#Domain(x)[t] ==> Unbox(t)-has-the-expected-type)

+        // (forall t: BoxType :: { Map#Elements(x)[t] }

+        //      Map#Domain(x)[t] ==> Unbox(Map#Elements(x)[t])-has-the-expected-type)

         Bpl.BoundVariable tVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$t#" + otherTmpVarCount, predef.BoxType));

         otherTmpVarCount++;

         Bpl.Expr t = new Bpl.IdentifierExpr(tok, tVar);

-        Bpl.Expr xSubT = Bpl.Expr.SelectTok(tok, FunctionCall(tok, BuiltinFunction.MapDomain, maptype, x), t);

-        Bpl.Expr xElemSubT = Bpl.Expr.SelectTok(tok, FunctionCall(tok, BuiltinFunction.MapElements, maptype, x), t);

+        Bpl.Expr inDomain = Bpl.Expr.SelectTok(tok, FunctionCall(tok, BuiltinFunction.MapDomain, maptype, x), t);

+        Bpl.Expr xAtT = Bpl.Expr.SelectTok(tok, FunctionCall(tok, BuiltinFunction.MapElements, maptype, x), t);

         Bpl.Expr unboxT = ExpressionTranslator.ModeledAsBoxType(mt.Domain) ? t : FunctionCall(tok, BuiltinFunction.Unbox, TrType(mt.Domain), t);

-        Bpl.Expr unboxElemT = ExpressionTranslator.ModeledAsBoxType(mt.Domain) ? xElemSubT : FunctionCall(tok, BuiltinFunction.Unbox, TrType(mt.Domain), xElemSubT);

+        Bpl.Expr unboxXAtT = ExpressionTranslator.ModeledAsBoxType(mt.Range) ? xAtT : FunctionCall(tok, BuiltinFunction.Unbox, TrType(mt.Range), xAtT);

 

         Bpl.Expr wh = GetWhereClause(tok, unboxT, mt.Domain, etran);

         if (wh != null) {

-          Bpl.Trigger tr = new Bpl.Trigger(tok, true, new Bpl.ExprSeq(xSubT));

-          clause = new Bpl.ForallExpr(tok, new Bpl.VariableSeq(tVar), tr, Bpl.Expr.Imp(xSubT, wh));

+          Bpl.Trigger tr = new Bpl.Trigger(tok, true, new Bpl.ExprSeq(inDomain));

+          clause = new Bpl.ForallExpr(tok, new Bpl.VariableSeq(tVar), tr, Bpl.Expr.Imp(inDomain, wh));

         }

 

-        Bpl.Expr wh2 = GetWhereClause(tok, xElemSubT, mt.Range, etran);

-        if (wh2 != null) {

-          Bpl.Trigger tr = new Bpl.Trigger(tok, true, new Bpl.ExprSeq(xElemSubT));

-          Bpl.Expr forall = new Bpl.ForallExpr(tok, new Bpl.VariableSeq(tVar), tr, Bpl.Expr.Imp(xSubT, wh));

+        wh = GetWhereClause(tok, unboxXAtT, mt.Range, etran);

+        if (wh != null) {

+          Bpl.Trigger tr = new Bpl.Trigger(tok, true, new Bpl.ExprSeq(xAtT));

+          Bpl.Expr forall = new Bpl.ForallExpr(tok, new Bpl.VariableSeq(tVar), tr, Bpl.Expr.Imp(inDomain, wh));

           if (clause == null) {

             clause = forall;

           } else {

@@ -7490,7 +7514,7 @@ namespace Microsoft.Dafny {
         } else if (expr is MapDisplayExpr) {

           MapDisplayExpr e = (MapDisplayExpr)expr;

           Bpl.Type maptype = predef.MapType(expr.tok, predef.BoxType, predef.BoxType);

-          Bpl.Expr s = translator.FunctionCall(expr.tok, "Map#Empty", maptype);

+          Bpl.Expr s = translator.FunctionCall(expr.tok, BuiltinFunction.MapEmpty, predef.BoxType);

           foreach (ExpressionPair p in e.Elements) {

             Bpl.Expr elt = BoxIfNecessary(expr.tok, TrExpr(p.A), cce.NonNull(p.A.Type));

             Bpl.Expr elt2 = BoxIfNecessary(expr.tok, TrExpr(p.B), cce.NonNull(p.B.Type));

@@ -8427,6 +8451,7 @@ namespace Microsoft.Dafny {
       SeqSameUntil,

       SeqFromArray,

 

+      MapEmpty,

       MapDomain,

       MapElements,

       MapEqual,

@@ -8615,6 +8640,12 @@ namespace Microsoft.Dafny {
           Contract.Assert(typeInstantiation != null);

           return FunctionCall(tok, "Seq#FromArray", typeInstantiation, args);

 

+        case BuiltinFunction.MapEmpty: {

+            Contract.Assert(args.Length == 0);

+            Contract.Assert(typeInstantiation != null);

+            Bpl.Type resultType = predef.MapType(tok, typeInstantiation, typeInstantiation);  // use 'typeInstantiation' (which is really always just BoxType anyway) as both type arguments

+            return Bpl.Expr.CoerceType(tok, FunctionCall(tok, "Map#Empty", resultType, args), resultType);

+          }

         case BuiltinFunction.MapDomain:

           Contract.Assert(args.Length == 1);

           return FunctionCall(tok, "Map#Domain", typeInstantiation, args);

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 72c142ac..68350abd 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -133,186 +133,6 @@ Execution trace:
 

 Dafny program verifier finished with 15 verified, 9 errors

 

--------------------- SmallTests.dfy --------------------

-SmallTests.dfy(30,11): Error: index out of range

-Execution trace:

-    (0,0): anon0

-SmallTests.dfy(61,36): Error: possible division by zero

-Execution trace:

-    (0,0): anon12_Then

-SmallTests.dfy(62,51): Error: possible division by zero

-Execution trace:

-    (0,0): anon12_Else

-    (0,0): anon3

-    (0,0): anon13_Else

-SmallTests.dfy(63,22): Error: target object may be null

-Execution trace:

-    (0,0): anon12_Then

-    (0,0): anon3

-    (0,0): anon13_Then

-    (0,0): anon6

-SmallTests.dfy(82,24): Error: target object may be null

-Execution trace:

-    (0,0): anon0

-    SmallTests.dfy(81,5): anon9_LoopHead

-    (0,0): anon9_LoopBody

-    (0,0): anon10_Then

-SmallTests.dfy(116,5): Error: call may violate context's modifies clause

-Execution trace:

-    (0,0): anon0

-    (0,0): anon4_Else

-    (0,0): anon3

-SmallTests.dfy(129,9): Error: call may violate context's modifies clause

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Then

-SmallTests.dfy(131,9): Error: call may violate context's modifies clause

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Else

-SmallTests.dfy(171,9): Error: assignment may update an object field not in the enclosing context's modifies clause

-Execution trace:

-    (0,0): anon0

-    (0,0): anon22_Else

-    (0,0): anon5

-    (0,0): anon24_Else

-    (0,0): anon11

-    (0,0): anon26_Else

-    (0,0): anon16

-    (0,0): anon28_Then

-    (0,0): anon29_Then

-    (0,0): anon19

-SmallTests.dfy(195,14): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon6_Then

-SmallTests.dfy(202,14): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon6_Else

-    (0,0): anon3

-    (0,0): anon7_Then

-SmallTests.dfy(204,14): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon6_Else

-    (0,0): anon3

-    (0,0): anon7_Else

-SmallTests.dfy(250,24): Error BP5002: A precondition for this call might not hold.

-SmallTests.dfy(228,30): Related location: This is the precondition that might not hold.

-Execution trace:

-    (0,0): anon0

-    SmallTests.dfy(245,19): anon3_Else

-    (0,0): anon2

-SmallTests.dfy(355,12): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-SmallTests.dfy(365,12): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-SmallTests.dfy(375,6): Error: cannot prove termination; try supplying a decreases clause

-Execution trace:

-    (0,0): anon3_Else

-SmallTests.dfy(638,14): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    SmallTests.dfy(635,5): anon7_LoopHead

-    (0,0): anon7_LoopBody

-    SmallTests.dfy(635,5): anon8_Else

-    (0,0): anon3

-    (0,0): anon9_Then

-    (0,0): anon6

-SmallTests.dfy(659,14): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon7_Then

-    (0,0): anon8_Then

-    (0,0): anon3

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

-SmallTests.dfy(279,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

-SmallTests.dfy(326,12): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon8_Then

-    (0,0): anon7

-SmallTests.dfy(333,10): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-SmallTests.dfy(343,4): Error: cannot prove termination; try supplying a decreases clause

-Execution trace:

-    (0,0): anon3_Else

-SmallTests.dfy(387,10): Error BP5003: A postcondition might not hold on this return path.

-SmallTests.dfy(390,41): Related location: This is the postcondition that might not hold.

-Execution trace:

-    (0,0): anon6_Else

-SmallTests.dfy(540,12): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Then

-    (0,0): anon2

-SmallTests.dfy(554,20): Error: left-hand sides 0 and 1 may refer to the same location

-Execution trace:

-    (0,0): anon0

-    (0,0): anon27_Then

-    (0,0): anon28_Then

-    (0,0): anon4

-    (0,0): anon29_Then

-    (0,0): anon30_Then

-    (0,0): anon9

-    (0,0): anon31_Then

-    (0,0): anon32_Then

-    (0,0): anon12

-SmallTests.dfy(556,15): Error: left-hand sides 1 and 2 may refer to the same location

-Execution trace:

-    (0,0): anon0

-    (0,0): anon27_Then

-    SmallTests.dfy(549,18): anon28_Else

-    (0,0): anon4

-    (0,0): anon29_Else

-    (0,0): anon7

-    (0,0): anon30_Then

-    (0,0): anon9

-    (0,0): anon31_Else

-    (0,0): anon35_Then

-    (0,0): anon36_Then

-    (0,0): anon37_Then

-    (0,0): anon22

-    (0,0): anon38_Then

-SmallTests.dfy(563,25): Error: target object may be null

-Execution trace:

-    (0,0): anon0

-SmallTests.dfy(576,10): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-SmallTests.dfy(604,10): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon8_Then

-    (0,0): anon9_Then

-    (0,0): anon4

-    (0,0): anon10_Then

-    (0,0): anon7

-SmallTests.dfy(618,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

-Execution trace:

-    (0,0): anon0

-    (0,0): anon5_Then

-    (0,0): anon6_Then

-    (0,0): anon3

-SmallTests.dfy(620,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

-Execution trace:

-    (0,0): anon0

-    (0,0): anon5_Else

-

-Dafny program verifier finished with 81 verified, 31 errors

-

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

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

 Execution trace:

@@ -1718,17 +1538,6 @@ Execution trace:
 

 Dafny program verifier finished with 11 verified, 4 errors

 

--------------------- LetExpr.dfy --------------------

-LetExpr.dfy(5,12): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-LetExpr.dfy(104,21): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon11_Then

-

-Dafny program verifier finished with 19 verified, 2 errors

-

 -------------------- Predicates.dfy --------------------

 Predicates.dfy[B](18,5): Error BP5003: A postcondition might not hold on this return path.

 Predicates.dfy[B](17,15): Related location: This is the postcondition that might not hold.

@@ -2033,16 +1842,16 @@ Execution trace:
 SmallTests.dfy(375,6): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

     (0,0): anon3_Else

-SmallTests.dfy(638,14): Error: assertion violation

+SmallTests.dfy(669,14): Error: assertion violation

 Execution trace:

     (0,0): anon0

-    SmallTests.dfy(635,5): anon7_LoopHead

+    SmallTests.dfy(666,5): anon7_LoopHead

     (0,0): anon7_LoopBody

-    SmallTests.dfy(635,5): anon8_Else

+    SmallTests.dfy(666,5): anon8_Else

     (0,0): anon3

     (0,0): anon9_Then

     (0,0): anon6

-SmallTests.dfy(659,14): Error: assertion violation

+SmallTests.dfy(690,14): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon7_Then

@@ -2112,7 +1921,10 @@ Execution trace:
 SmallTests.dfy(576,10): Error: assertion violation

 Execution trace:

     (0,0): anon0

-SmallTests.dfy(604,10): Error: assertion violation

+SmallTests.dfy(600,5): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

+Execution trace:

+    (0,0): anon0

+SmallTests.dfy(623,10): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon8_Then

@@ -2120,18 +1932,21 @@ Execution trace:
     (0,0): anon4

     (0,0): anon10_Then

     (0,0): anon7

-SmallTests.dfy(618,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

+SmallTests.dfy(637,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

 Execution trace:

     (0,0): anon0

     (0,0): anon5_Then

     (0,0): anon6_Then

     (0,0): anon3

-SmallTests.dfy(620,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

+SmallTests.dfy(639,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

 Execution trace:

     (0,0): anon0

     (0,0): anon5_Else

+SmallTests.dfy(652,9): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

+Execution trace:

+    (0,0): anon0

 

-Dafny program verifier finished with 81 verified, 31 errors

+Dafny program verifier finished with 85 verified, 33 errors

 out.tmp.dfy(33,11): Error: index out of range

 Execution trace:

     (0,0): anon0

@@ -2211,23 +2026,23 @@ Execution trace:
 out.tmp.dfy(285,6): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

     (0,0): anon3_Else

-out.tmp.dfy(386,14): Error: assertion violation

+out.tmp.dfy(388,14): Error: assertion violation

 Execution trace:

     (0,0): anon0

-    out.tmp.dfy(382,5): anon7_LoopHead

+    out.tmp.dfy(384,5): anon7_LoopHead

     (0,0): anon7_LoopBody

-    out.tmp.dfy(382,5): anon8_Else

+    out.tmp.dfy(384,5): anon8_Else

     (0,0): anon3

     (0,0): anon9_Then

     (0,0): anon6

-out.tmp.dfy(412,14): Error: assertion violation

+out.tmp.dfy(414,14): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon7_Then

     (0,0): anon8_Then

     (0,0): anon3

-out.tmp.dfy(449,3): Error BP5003: A postcondition might not hold on this return path.

-out.tmp.dfy(443,11): Related location: This is the postcondition that might not hold.

+out.tmp.dfy(451,3): Error BP5003: A postcondition might not hold on this return path.

+out.tmp.dfy(445,11): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

     (0,0): anon18_Else

@@ -2236,27 +2051,27 @@ Execution trace:
     (0,0): anon24_Then

     (0,0): anon15

     (0,0): anon25_Else

-out.tmp.dfy(473,12): Error: assertion violation

+out.tmp.dfy(475,12): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon8_Then

     (0,0): anon7

-out.tmp.dfy(478,10): Error: assertion violation

+out.tmp.dfy(480,10): Error: assertion violation

 Execution trace:

     (0,0): anon0

-out.tmp.dfy(488,4): Error: cannot prove termination; try supplying a decreases clause

+out.tmp.dfy(490,4): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

     (0,0): anon3_Else

-out.tmp.dfy(496,10): Error BP5003: A postcondition might not hold on this return path.

-out.tmp.dfy(497,41): Related location: This is the postcondition that might not hold.

+out.tmp.dfy(498,10): Error BP5003: A postcondition might not hold on this return path.

+out.tmp.dfy(499,41): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon6_Else

-out.tmp.dfy(534,12): Error: assertion violation

+out.tmp.dfy(536,12): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Then

     (0,0): anon2

-out.tmp.dfy(548,20): Error: left-hand sides 0 and 1 may refer to the same location

+out.tmp.dfy(550,20): Error: left-hand sides 0 and 1 may refer to the same location

 Execution trace:

     (0,0): anon0

     (0,0): anon27_Then

@@ -2268,11 +2083,11 @@ Execution trace:
     (0,0): anon31_Then

     (0,0): anon32_Then

     (0,0): anon12

-out.tmp.dfy(550,15): Error: left-hand sides 1 and 2 may refer to the same location

+out.tmp.dfy(552,15): Error: left-hand sides 1 and 2 may refer to the same location

 Execution trace:

     (0,0): anon0

     (0,0): anon27_Then

-    out.tmp.dfy(543,17): anon28_Else

+    out.tmp.dfy(545,17): anon28_Else

     (0,0): anon4

     (0,0): anon29_Else

     (0,0): anon7

@@ -2284,13 +2099,16 @@ Execution trace:
     (0,0): anon37_Then

     (0,0): anon22

     (0,0): anon38_Then

-out.tmp.dfy(557,25): Error: target object may be null

+out.tmp.dfy(559,25): Error: target object may be null

+Execution trace:

+    (0,0): anon0

+out.tmp.dfy(572,10): Error: assertion violation

 Execution trace:

     (0,0): anon0

-out.tmp.dfy(570,10): Error: assertion violation

+out.tmp.dfy(598,5): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

 Execution trace:

     (0,0): anon0

-out.tmp.dfy(597,10): Error: assertion violation

+out.tmp.dfy(617,10): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon8_Then

@@ -2298,18 +2116,21 @@ Execution trace:
     (0,0): anon4

     (0,0): anon10_Then

     (0,0): anon7

-out.tmp.dfy(611,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

+out.tmp.dfy(631,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

 Execution trace:

     (0,0): anon0

     (0,0): anon5_Then

     (0,0): anon6_Then

     (0,0): anon3

-out.tmp.dfy(613,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

+out.tmp.dfy(633,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

 Execution trace:

     (0,0): anon0

     (0,0): anon5_Else

+out.tmp.dfy(647,9): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

+Execution trace:

+    (0,0): anon0

 

-Dafny program verifier finished with 81 verified, 31 errors

+Dafny program verifier finished with 85 verified, 33 errors

 

 -------------------- LetExpr.dfy --------------------

 LetExpr.dfy(5,12): Error: assertion violation

diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index d9b91763..7b88d0d4 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -588,6 +588,25 @@ method AssignSuchThat7<T>(A: set<T>, x: T) {
   assert x in A ==> x in B;

 }

 

+method AssignSuchThat8(n: int) returns (x: int, y: Lindgren) {

+  x :| x in {1};

+  x :| x in {3, 7, 11};

+  x :| x in {n + 12};

+  y :| y in {HerrNilsson};

+  y :| y == y;

+  x :| x in multiset{3, 3, 2, 3};

+  x :| x in map[5 := 10, 6 := 12];

+  x :| x in [n, n, 2];

+  x :| x in [];  // error

+}

+

+codatatype QuiteFinite = QQA | QQB | QQC;

+

+method AssignSuchThat9() returns (q: QuiteFinite)

+{

+  q :| q != QQA && q != QQC;

+}

+

 // ----------- let-such-that expressions ------------------------

 

 function method LetSuchThat_P(x: int): bool

@@ -621,6 +640,18 @@ method LetSuchThat2(n: nat)
   }

 }

 

+ghost method LetSuchThat3(n: int) returns (xx: int, yy: Lindgren) {

+  xx := var x :| x in {1}; x+10;

+  xx := var x :| x in {3, 7, 11}; x+10;

+  xx := var x :| x in {n + 12}; x+10;

+  yy := var y :| y in {HerrNilsson}; y;

+  yy := var y :| y == y; y;

+  xx := var x :| x in multiset{3, 3, 2, 3}; x+10;

+  xx := var x :| x in map[5 := 10, 6 := 12]; x+10;

+  xx := var x :| x in [n, n, 2]; x+10;

+  xx := var x :| x in map[]; x+10;  // error

+}

+

 // ------------- ghost loops only modify ghost fields

 

 class GT {

diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index 82d4bebd..1bb2ef9f 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -10,7 +10,7 @@ for %%f in (Simple.dfy) do (
   %DAFNY_EXE% %* /dprint:- /env:0 /noVerify %%f

 )

 

-for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy

+for %%f in (TypeTests.dfy NatTypes.dfy Definedness.dfy

             FunctionSpecifications.dfy ResolutionErrors.dfy ParseErrors.dfy

             Array.dfy MultiDimArray.dfy NonGhostQuantifiers.dfy AdvancedLHS.dfy

             ModulesCycle.dfy Modules0.dfy Modules1.dfy Modules2.dfy BadFunction.dfy

@@ -22,7 +22,7 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy
             TypeAntecedents.dfy NoTypeArgs.dfy EqualityTypes.dfy SplitExpr.dfy

             LoopModifies.dfy Refinement.dfy RefinementErrors.dfy

             ReturnErrors.dfy ReturnTests.dfy ChainingDisjointTests.dfy

-            CallStmtTests.dfy MultiSets.dfy PredExpr.dfy LetExpr.dfy

+            CallStmtTests.dfy MultiSets.dfy PredExpr.dfy

             Predicates.dfy Skeletons.dfy Maps.dfy LiberalEquality.dfy

             RefinementModificationChecking.dfy TailCalls.dfy

             Calculations.dfy IteratorResolution.dfy Iterators.dfy) do (

@@ -40,7 +40,7 @@ for %%f in (Superposition.dfy) do (
 for %%f in (SmallTests.dfy LetExpr.dfy) do (

   echo.

   echo -------------------- %%f --------------------

-  %DAFNY_EXE% /compile:0 /dprint:out.tmp.dfy %* %%f

+  %DAFNY_EXE% /compile:0 /print:out.bpl.tmp /dprint:out.tmp.dfy %* %%f

   %DAFNY_EXE% /compile:0 %* out.tmp.dfy

 )