Merge

16 files changed, 128 insertions, 87 deletions

diff --git a/BCT/BytecodeTranslator/StatementTraverser.cs b/BCT/BytecodeTranslator/StatementTraverser.cs
index 0dc7c5ab..6bc399c1 100644
--- a/BCT/BytecodeTranslator/StatementTraverser.cs
+++ b/BCT/BytecodeTranslator/StatementTraverser.cs
@@ -106,6 +106,7 @@ namespace BytecodeTranslator
           elseIfCmd = new Bpl.IfCmd(Bpl.Token.NoToken, Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq, labelExpr, targetExpr), TranslationHelper.BuildStmtList(gotoCmd), elseIfCmd, null);

         }

         this.StmtBuilder.Add(elseIfCmd);

+        this.StmtBuilder.Add(new Bpl.AssumeCmd(Bpl.Token.NoToken, Bpl.Expr.Literal(false)));

       }

     }

     #endregion

diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala
index b1aaeea9..ea05d4bc 100644
--- a/Chalice/src/Translator.scala
+++ b/Chalice/src/Translator.scala
@@ -1449,7 +1449,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
         val (tmpHeapV, tmpHeap) = Boogie.NewBVar("Heap", theap, true);

         val (tmpMaskV, tmpMask) = Boogie.NewBVar("Mask", tmask, true); 

         val (tmpCreditsV, tmpCredits) = Boogie.NewBVar("Credits", tcredits, true); 

-        val tmpTranslator = new ExpressionTranslator(List(tmpHeap,tmpMask,tmpCredits), currentClass);

+        val tmpTranslator = new ExpressionTranslator(List(tmpHeap,tmpMask,tmpCredits), etran.oldEtran.Globals, currentClass);

         

         // pick new k

         val (funcappKV, funcappK) = Boogie.NewBVar("funcappK", tint, true)

@@ -1475,7 +1475,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
         val (tmpHeapV, tmpHeap) = Boogie.NewBVar("Heap", theap, true);

         val (tmpMaskV, tmpMask) = Boogie.NewBVar("Mask", tmask, true);

         val (tmpCreditsV, tmpCredits) = Boogie.NewBVar("Credits", tcredits, true);

-        val tmpTranslator = new ExpressionTranslator(List(tmpHeap, tmpMask, tmpCredits), currentClass);

+        val tmpTranslator = new ExpressionTranslator(List(tmpHeap, tmpMask, tmpCredits), etran.oldEtran.Globals, currentClass);

         

         val receiverOk = isDefined(obj) ::: prove(nonNull(Tr(obj)), obj.pos, "Receiver might be null.");

         val definition = scaleExpressionByPermission(SubstThis(DefinitionOf(pred.predicate), obj), perm, unfolding.pos)

@@ -1549,7 +1549,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
         isDefined(e0) ::: isDefined(e1)

       case Eval(h, e) =>

         val (evalHeap, evalMask, evalCredits, checks, assumptions) = fromEvalState(h);

-        val evalEtran = new ExpressionTranslator(List(evalHeap, evalMask, evalCredits), currentClass);

+        val evalEtran = new ExpressionTranslator(List(evalHeap, evalMask, evalCredits), etran.oldEtran.Globals, currentClass);

         evalEtran.isDefined(e)

       case _ : SeqQuantification => throw new InternalErrorException("should be desugared")

       case tq @ TypeQuantification(_, _, _, e, (min, max)) =>

@@ -1675,7 +1675,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
     case Contains(e0, e1) => SeqContains(Tr(e1), Tr(e0))

     case Eval(h, e) =>

       val (evalHeap, evalMask, evalCredits, checks, assumptions) = fromEvalState(h);

-      val evalEtran = new ExpressionTranslator(List(evalHeap, evalMask, evalCredits), currentClass);

+      val evalEtran = new ExpressionTranslator(List(evalHeap, evalMask, evalCredits), etran.oldEtran.Globals, currentClass);

       evalEtran.Tr(e)

     case _:SeqQuantification => throw new InternalErrorException("should be desugared")

     case tq @ TypeQuantification(Forall, _, _, e, _) =>

@@ -1746,10 +1746,10 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
   }

 

   def Inhale(p: Expression, ih: Boogie.Expr, check: Boolean, currentK: Expr): List[Boogie.Stmt] = desugar(p) match {

-    case pred@MemberAccess(e, p) if pred.isPredicate => 
-      val chk = (if (check) {
-        isDefined(e)(true) ::: 
-        bassert(nonNull(Tr(e)), e.pos, "Receiver might be null.") :: Nil
+    case pred@MemberAccess(e, p) if pred.isPredicate => 

+      val chk = (if (check) {

+        isDefined(e)(true) ::: 

+        bassert(nonNull(Tr(e)), e.pos, "Receiver might be null.") :: Nil

       } else Nil)

       val tmp = Access(pred, Full);

       tmp.pos = pred.pos;

@@ -2393,6 +2393,7 @@ object TranslationHelper {
   // scale an expression (such as the definition of a predicate) by a permission

   def scaleExpressionByPermission(expr: Expression, perm1: Permission, pos: Position): Expression = {

     val result = expr match {

+      case pred@MemberAccess(o, p) if pred.isPredicate => Access(pred, perm1)

       case Access(e, perm2) => Access(e, multiplyPermission(perm1, perm2, pos))

       case AccessSeq(e, f, perm2) => AccessSeq(e, f, multiplyPermission(perm1, perm2, pos))

       case And(lhs, rhs) => And(scaleExpressionByPermission(lhs, perm1, pos), scaleExpressionByPermission(rhs, perm1, pos))

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 7f5642f3..3a80a2ea 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -697,52 +697,14 @@ namespace Microsoft.Boogie {
       }

       return g;

     }

-

-    // Delete unreachable Blocks of an Impl. This helps avoid a bug inside

-    // NewComputeDominators

-

-    public void pruneUnreachableBlocks(Implementation impl)

-    {

-        // Do a BFS to find all reachable blocks

-        List<Block> reachableBlocks = new List<Block>();

-        HashSet<string> visited = new HashSet<string>();

-        List<Block> worklist = new List<Block>();

-

-        visited.Add(impl.Blocks[0].Label);

-        worklist.Add(impl.Blocks[0]);

-

-        while (worklist.Count != 0)

-        {

-            var block = worklist[0];

-            worklist.RemoveAt(0);

-

-            reachableBlocks.Add(block);

-            GotoCmd gc = block.TransferCmd as GotoCmd;

-            if(gc == null) continue;

-

-            foreach (Block succ in gc.labelTargets)

-            {

-                if (visited.Contains(succ.Label)) continue;

-                visited.Add(succ.Label);

-                worklist.Add(succ);

-            }

-        }

-

-        // Delete unreachable blocks

-       

-        // Make sure that the start block hasn't changed.

-        Contract.Assert(reachableBlocks[0] == impl.Blocks[0]);

-

-        impl.Blocks = reachableBlocks;

-    }

-

+    

     public Dictionary<string, Dictionary<string, Block>> ExtractLoops() {

       List<Implementation/*!*/>/*!*/ loopImpls = new List<Implementation/*!*/>();

       Dictionary<string, Dictionary<string, Block>> fullMap = new Dictionary<string, Dictionary<string, Block>>();

       foreach (Declaration d in this.TopLevelDeclarations) {

         Implementation impl = d as Implementation;

         if (impl != null && impl.Blocks != null && impl.Blocks.Count > 0) {

-          pruneUnreachableBlocks(impl);

+          impl.PruneUnreachableBlocks();

           Graph<Block/*!*/>/*!*/ g = GraphFromImpl(impl);

           g.ComputeLoops();

           if (!g.Reducible) {

diff --git a/Source/Core/VCExp.cs b/Source/Core/VCExp.cs
index be6695e8..5b7fc946 100644
--- a/Source/Core/VCExp.cs
+++ b/Source/Core/VCExp.cs
@@ -113,7 +113,7 @@ The generic options may or may not be used by the prover plugin.
         if (opt.Length == name.Length) {

           field = "";

           return true;

-        } else if (opt[name.Length] == '=') {

+        } else if (opt[name.Length] == '=' || opt[name.Length] == ':') {

           field = opt.Substring(name.Length + 1);

           return true;

         }

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index ac573660..f6e40722 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -1060,18 +1060,22 @@ OrOp = "||" | '\u2228'.
 /*------------------------------------------------------------------------*/

 RelationalExpression<out Expression/*!*/ e>

 = (. Contract.Ensures(Contract.ValueAtReturn(out e) != null);

-     IToken x, firstOpTok = null;  Expression e0, e1;  BinaryExpr.Opcode op;

+     IToken x, firstOpTok = null;  Expression e0, e1, acc = null;  BinaryExpr.Opcode op;

      List<Expression> chain = null;

      List<BinaryExpr.Opcode> ops = null;

      int kind = 0;  // 0 ("uncommitted") indicates chain of ==, possibly with one !=

                     // 1 ("ascending")   indicates chain of ==, <, <=, possibly with one !=

                     // 2 ("descending")  indicates chain of ==, >, >=, possibly with one !=

                     // 3 ("illegal")     indicates illegal chain

+                    // 4 ("disjoint")    indicates chain of disjoint set operators

      bool hasSeenNeq = false;

   .)

   Term<out e0>                     (. e = e0; .)

   [ RelOp<out x, out op>           (. firstOpTok = x; .)

-    Term<out e1>                   (. e = new BinaryExpr(x, op, e0, e1); .)

+    Term<out e1>                   (. e = new BinaryExpr(x, op, e0, e1);

+                                      if (op == BinaryExpr.Opcode.Disjoint)

+                                        acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, e0, e1); // accumulate first two operands.

+                                   .)

     {                              (. if (chain == null) {

                                         chain = new List<Expression>();

                                         ops = new List<BinaryExpr.Opcode>();

@@ -1087,6 +1091,8 @@ RelationalExpression<out Expression/*!*/ e>
                                           case BinaryExpr.Opcode.Gt:

                                           case BinaryExpr.Opcode.Ge:

                                             kind = 2;  break;

+                                          case BinaryExpr.Opcode.Disjoint:

+                                            kind = 4;  break;

                                           default:

                                             kind = 3;  break;

                                         }

@@ -1095,10 +1101,11 @@ RelationalExpression<out Expression/*!*/ e>
                                    .)

       RelOp<out x, out op>         (. switch (op) {

                                         case BinaryExpr.Opcode.Eq:

-                                          if (kind == 3) { SemErr(x, "chaining not allowed from the previous operator"); }

+                                          if (kind != 0 && kind != 1 && kind != 2) { SemErr(x, "chaining not allowed from the previous operator"); }

                                           break;

                                         case BinaryExpr.Opcode.Neq:

                                           if (hasSeenNeq) { SemErr(x, "a chain cannot have more than one != operator"); }

+                                          if (kind != 0 && kind != 1 && kind != 2) { SemErr(x, "this operator cannot continue this chain"); }

                                           hasSeenNeq = true;  break;

                                         case BinaryExpr.Opcode.Lt:

                                         case BinaryExpr.Opcode.Le:

@@ -1110,13 +1117,21 @@ RelationalExpression<out Expression/*!*/ e>
                                           if (kind == 0) { kind = 2; }

                                           else if (kind != 2) { SemErr(x, "this operator chain cannot continue with a descending operator"); }

                                           break;

+                                        case BinaryExpr.Opcode.Disjoint:

+                                          if (kind != 4) { SemErr(x, "can only chain disjoint (!!) with itself."); kind = 3; }

+                                          break;

                                         default:

                                           SemErr(x, "this operator cannot be part of a chain");

                                           kind = 3;  break;

                                       }

                                    .)

       Term<out e1>                 (. ops.Add(op); chain.Add(e1);

-                                      e = new BinaryExpr(x, BinaryExpr.Opcode.And, e, new BinaryExpr(x, op, e0, e1));

+                                      if (op == BinaryExpr.Opcode.Disjoint) {

+                                        e = new BinaryExpr(x, BinaryExpr.Opcode.And, e, new BinaryExpr(x, op, acc, e1));

+                                        acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, acc, e1); //e0 has already been added.

+                                      }

+                                      else

+                                        e = new BinaryExpr(x, BinaryExpr.Opcode.And, e, new BinaryExpr(x, op, e0, e1));

                                    .)

     }

   ]

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index f9bb0768..e12ab7e3 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -1552,13 +1552,14 @@ List<Expression/*!*/>/*!*/ decreases) {
 

 	void RelationalExpression(out Expression/*!*/ e) {

 		Contract.Ensures(Contract.ValueAtReturn(out e) != null);

-		IToken x, firstOpTok = null;  Expression e0, e1;  BinaryExpr.Opcode op;

+		IToken x, firstOpTok = null;  Expression e0, e1, acc = null;  BinaryExpr.Opcode op;

 		List<Expression> chain = null;

 		List<BinaryExpr.Opcode> ops = null;

 		int kind = 0;  // 0 ("uncommitted") indicates chain of ==, possibly with one !=

 		               // 1 ("ascending")   indicates chain of ==, <, <=, possibly with one !=

 		               // 2 ("descending")  indicates chain of ==, >, >=, possibly with one !=

 		               // 3 ("illegal")     indicates illegal chain

+		               // 4 ("disjoint")    indicates chain of disjoint set operators

 		bool hasSeenNeq = false;

 		

 		Term(out e0);

@@ -1567,7 +1568,10 @@ List<Expression/*!*/>/*!*/ decreases) {
 			RelOp(out x, out op);

 			firstOpTok = x; 

 			Term(out e1);

-			e = new BinaryExpr(x, op, e0, e1); 

+			e = new BinaryExpr(x, op, e0, e1);

+			if (op == BinaryExpr.Opcode.Disjoint)

+			acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, e0, e1); // accumulate first two operands.

+			

 			while (StartOf(16)) {

 				if (chain == null) {

 				 chain = new List<Expression>();

@@ -1584,6 +1588,8 @@ List<Expression/*!*/>/*!*/ decreases) {
 				   case BinaryExpr.Opcode.Gt:

 				   case BinaryExpr.Opcode.Ge:

 				     kind = 2;  break;

+				   case BinaryExpr.Opcode.Disjoint:

+				     kind = 4;  break;

 				   default:

 				     kind = 3;  break;

 				 }

@@ -1593,30 +1599,40 @@ List<Expression/*!*/>/*!*/ decreases) {
 				RelOp(out x, out op);

 				switch (op) {

 				 case BinaryExpr.Opcode.Eq:

-				   if (kind == 3) { SemErr(x, "chaining not allowed from the previous operator"); }

+				   if (kind != 0 && kind != 1 && kind != 2) { SemErr(x, "chaining not allowed from the previous operator"); }

 				   break;

 				 case BinaryExpr.Opcode.Neq:

 				   if (hasSeenNeq) { SemErr(x, "a chain cannot have more than one != operator"); }

-				   hasSeenNeq = true;  break;

-				 case BinaryExpr.Opcode.Lt:

-				 case BinaryExpr.Opcode.Le:

-				   if (kind == 0) { kind = 1; }

-				   else if (kind != 1) { SemErr(x, "this operator chain cannot continue with an ascending operator"); }

-				   break;

-				 case BinaryExpr.Opcode.Gt:

-				 case BinaryExpr.Opcode.Ge:

-				   if (kind == 0) { kind = 2; }

-				   else if (kind != 2) { SemErr(x, "this operator chain cannot continue with a descending operator"); }

-				   break;

-				 default:

-				   SemErr(x, "this operator cannot be part of a chain");

-				   kind = 3;  break;

-				}

-				

+				if (kind != 0 && kind != 1 && kind != 2) { SemErr(x, "this operator cannot continue this chain"); }

+				                              hasSeenNeq = true;  break;

+				                            case BinaryExpr.Opcode.Lt:

+				                            case BinaryExpr.Opcode.Le:

+				                              if (kind == 0) { kind = 1; }

+				                              else if (kind != 1) { SemErr(x, "this operator chain cannot continue with an ascending operator"); }

+				                              break;

+				                            case BinaryExpr.Opcode.Gt:

+				                            case BinaryExpr.Opcode.Ge:

+				                              if (kind == 0) { kind = 2; }

+				                              else if (kind != 2) { SemErr(x, "this operator chain cannot continue with a descending operator"); }

+				                              break;

+				                            case BinaryExpr.Opcode.Disjoint:

+				                              if (kind != 4) { SemErr(x, "can only chain disjoint (!!) with itself."); kind = 3; }

+				break;

+				                            default:

+				                              SemErr(x, "this operator cannot be part of a chain");

+				                              kind = 3;  break;

+				                          }

+				                       

 				Term(out e1);

 				ops.Add(op); chain.Add(e1);

-				e = new BinaryExpr(x, BinaryExpr.Opcode.And, e, new BinaryExpr(x, op, e0, e1));

-				

+				if (op == BinaryExpr.Opcode.Disjoint)

+				{

+				  e = new BinaryExpr(x, BinaryExpr.Opcode.And, e, new BinaryExpr(x, op, acc, e1));

+				acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, acc, e1); //e0 has already been added.

+				    }

+				 else

+				   e = new BinaryExpr(x, BinaryExpr.Opcode.And, e, new BinaryExpr(x, op, e0, e1));

+				                         

 			}

 		}

 		if (chain != null) {

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index 42cf89ab..bc137492 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -152,10 +152,8 @@ namespace Microsoft.Boogie.SMTLib
           SendCommon("(set-option :" + opt.Option + " " + opt.Value + ")");

         }

 

-        if (CommandLineOptions.Clo.UseArrayTheory) {

-          SendCommon("; skipping logic setting (using arrays)");

-        } else {

-          SendCommon("(set-logic UFNIA)");

+        if (!string.IsNullOrEmpty(options.Logic)) {

+          SendCommon("(set-logic " + options.Logic + ")");

         }

 

         SendCommon("; done setting options\n");

@@ -348,8 +346,10 @@ namespace Microsoft.Boogie.SMTLib
             posLabels = Enumerable.Empty<string>();

           var conjuncts = posLabels.Select(s => "(not " + lbl(s) + ")").Concat(negLabels.Select(lbl)).ToArray();

           var expr = conjuncts.Length == 1 ? conjuncts[0] : ("(or " + conjuncts.Concat(" ") + ")");

-          SendThisVC("(assert " + expr + ")");

-          SendThisVC("(check-sat)");

+          if (errorsLeft > 0) {

+            SendThisVC("(assert " + expr + ")");

+            SendThisVC("(check-sat)");

+          }

         }

 

         SendThisVC("(pop 1)");

diff --git a/Source/Provers/SMTLib/SMTLibNamer.cs b/Source/Provers/SMTLib/SMTLibNamer.cs
index 0793c614..a874c6c5 100644
--- a/Source/Provers/SMTLib/SMTLibNamer.cs
+++ b/Source/Provers/SMTLib/SMTLibNamer.cs
@@ -27,6 +27,9 @@ namespace Microsoft.Boogie.SMTLib
       // Bitvectors

       "extract", "concat", 

       "bvnot", "bvneg", "bvand", "bvor", "bvadd", "bvmul", "bvudiv", "bvurem", "bvshl", "bvlshr", "bvult",

+      // arrays

+      "store", "select", "const", "default", "map", "union", "intersect", "difference", "complement",

+      "subset", "array-ext", "as-array", "Array",

       // Z3 (and not only?) extensions to bitvectors

       "bit1", "bit0", "bvsub", "bvsdiv", "bvsrem", "bvsmod", "bvsdiv0", "bvudiv0", "bvsrem0", "bvurem0",

       "bvsmod0", "bvsdiv_i", "bvudiv_i", "bvsrem_i", "bvurem_i", "bvumod_i", "bvule", "bvsle", "bvuge",

diff --git a/Source/Provers/SMTLib/SMTLibProverOptions.cs b/Source/Provers/SMTLib/SMTLibProverOptions.cs
index 44f91cc2..653b2c15 100644
--- a/Source/Provers/SMTLib/SMTLibProverOptions.cs
+++ b/Source/Provers/SMTLib/SMTLibProverOptions.cs
@@ -34,6 +34,7 @@ namespace Microsoft.Boogie.SMTLib
     public List<OptionValue> SmtOptions = new List<OptionValue>();

     public List<string> SolverArguments = new List<string>();

     public bool MultiTraces = false;

+    public string Logic = "";

 

     // Z3 specific (at the moment; some of them make sense also for other provers)

     public bool UseZ3 = true;

@@ -92,6 +93,7 @@ namespace Microsoft.Boogie.SMTLib
         ParseBool(opt, "USE_Z3", ref UseZ3) ||

         ParseString(opt, "INSPECTOR", ref Inspector) ||

         ParseBool(opt, "OPTIMIZE_FOR_BV", ref OptimizeForBv) ||

+        ParseString(opt, "LOGIC", ref Logic) ||

         base.Parse(opt);

     }

 

@@ -114,6 +116,7 @@ USE_WEIGHTS=<bool>        Pass :weight annotations on quantified formulas (defau
 VERBOSITY=<int>           1 - print prover output (default: 0)

 O:<name>=<value>          Pass (set-option :<name> <value>) to the SMT solver.

 C:<string>                Pass <string> to the SMT on the command line. 

+LOGIC=<string>            Pass (set-logic <string>) to the prover (default: empty)

 

 Z3-specific options:

 ~~~~~~~~~~~~~~~~~~~~

diff --git a/Source/Provers/SMTLib/Z3.cs b/Source/Provers/SMTLib/Z3.cs
index 54742802..da9e8faa 100644
--- a/Source/Provers/SMTLib/Z3.cs
+++ b/Source/Provers/SMTLib/Z3.cs
@@ -157,8 +157,10 @@ namespace Microsoft.Boogie.SMTLib
         options.AddWeakSmtOption("WARNING", "false");

       }

 

-      if (options.TimeLimit > 0)

+      if (options.TimeLimit > 0) {

         options.AddWeakSmtOption("SOFT_TIMEOUT", options.TimeLimit.ToString());

+        options.AddSolverArgument("/T:" + (options.TimeLimit + 1000) / 1000);

+      }

 

       // legacy option handling

       if (!CommandLineOptions.Clo.z3AtFlag)

diff --git a/Source/Provers/Z3/Prover.cs b/Source/Provers/Z3/Prover.cs
index 83294381..640f98ae 100644
--- a/Source/Provers/Z3/Prover.cs
+++ b/Source/Provers/Z3/Prover.cs
@@ -4,7 +4,7 @@
 //

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

 

-//#define RECENT_Z3 // 2.20 or newer

+// #define RECENT_Z3 // 2.20 or newer

 

 using System;

 using System.IO;

@@ -135,7 +135,9 @@ namespace Microsoft.Boogie.Z3
         AddOption(result, "ARITH_RANDOM_INITIAL_VALUE", "true");

 

         // The left-to-right structural case-splitting strategy.

+#if !RECENT_Z3

         AddOption(result, "SORT_AND_OR", "false");

+#endif

         AddOption(result, "CASE_SPLIT", "3");

 

         // In addition delay adding unit conflicts.

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 384037ae..e5621773 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -450,12 +450,11 @@ ParseErrors.dfy(4,19): error: a chain cannot have more than one != operator
 ParseErrors.dfy(6,37): error: this operator chain cannot continue with a descending operator

 ParseErrors.dfy(7,38): error: this operator chain cannot continue with an ascending operator

 ParseErrors.dfy(12,24): error: this operator chain cannot continue with a descending operator

-ParseErrors.dfy(14,18): error: this operator cannot be part of a chain

 ParseErrors.dfy(15,18): error: this operator cannot be part of a chain

 ParseErrors.dfy(16,19): error: this operator cannot be part of a chain

 ParseErrors.dfy(17,18): error: this operator cannot be part of a chain

 ParseErrors.dfy(18,18): error: chaining not allowed from the previous operator

-9 parse errors detected in ParseErrors.dfy

+8 parse errors detected in ParseErrors.dfy

 

 -------------------- Array.dfy --------------------

 Array.dfy(10,8): Error: assignment may update an array element not in the enclosing context's modifies clause

@@ -1100,3 +1099,7 @@ ReturnErrors.dfy(41,10): Error: can only have initialization methods which modif
 -------------------- ReturnTests.dfy --------------------

 

 Dafny program verifier finished with 16 verified, 0 errors

+

+-------------------- ChainingDisjointTests.dfy --------------------

+

+Dafny program verifier finished with 6 verified, 0 errors

diff --git a/Test/dafny0/ChainingDisjointTests.dfy b/Test/dafny0/ChainingDisjointTests.dfy
new file mode 100644
index 00000000..17a4fa9f
--- /dev/null
+++ b/Test/dafny0/ChainingDisjointTests.dfy
@@ -0,0 +1,33 @@
+

+method testing1() 

+{

+   var a, b, c := {1,2}, {3, 4}, {5, 6};

+   assert a !! b !! c;

+   testing2(a, b, c);

+   assert !({1,2} !! {2,3});

+   assert !({1,2} !! {9} !! {2,3}); // tests the accumulation

+   assert !({1,2} !! {9} !! {2,3});

+   assert !({1,2} !! {9} !! {8} !! {2,3}); // doesn't break at 4. that seems like a good stopping place.

+   assert !({9} !! {1,2} !! {8} !! {2,3});

+   assert !({9} !! {1} + {2} !! {8} !! {2,3}); // mixing in some other operators

+   assert !({1} !! {1} + {2});

+}

+

+method testing2(a: set<int>, b: set<int>, c: set<int>)

+   requires a !! b !! c;

+{

+   assert a !! b;

+   assert a !! c;

+   assert b !! c;

+}

+

+method testing3(a: set<int>, b: set<int>, c: set<int>, d: set<int>) // again with the four.

+   requires a !! b !! c !! d;

+{

+   assert a !! b;

+   assert a !! c;

+   assert b !! c;

+   assert a !! d;

+   assert b !! d;

+   assert c !! d;

+}

diff --git a/Test/dafny0/ParseErrors.dfy b/Test/dafny0/ParseErrors.dfy
index d6f3005d..41df50eb 100644
--- a/Test/dafny0/ParseErrors.dfy
+++ b/Test/dafny0/ParseErrors.dfy
@@ -11,7 +11,7 @@ method TestChaining0(j: int, k: int, m: int)
 method TestChaining1<T>(s: set<T>, t: set<T>, u: set<T>, x: T, SuperSet: set<set<T>>)

   requires s <= t <= u >= s+u;  // error: cannot mix <= and >=

   ensures s <= u;

-  ensures s !! t !! u;  // error: !! is not chaining (but it would be nice if it were)

+  ensures s !! t !! u; // valid, means pairwise disjoint

   ensures x in s in SuperSet;  // error: 'in' is not chaining

   ensures x !in s in SuperSet;  // error: 'in' is not chaining

   ensures x in s !in SuperSet;  // error: 'in' is not chaining

diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index f606c183..143a0dc5 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -19,7 +19,7 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy
             Termination.dfy DTypes.dfy

             TypeParameters.dfy Datatypes.dfy TypeAntecedents.dfy SplitExpr.dfy

             Refinement.dfy RefinementErrors.dfy LoopModifies.dfy

-            ReturnErrors.dfy ReturnTests.dfy) do (

+            ReturnErrors.dfy ReturnTests.dfy ChainingDisjointTests.dfy) do (

   echo.

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

   %DAFNY_EXE% /compile:0 %* %%f

diff --git a/Test/runtest.bat b/Test/runtest.bat
index 4b751a6c..5b3d45ae 100644
--- a/Test/runtest.bat
+++ b/Test/runtest.bat
@@ -5,7 +5,7 @@ if not exist %1\nul goto noDirExists
 echo ----- Running regression test %1

 pushd %1

 if not exist runtest.bat goto noRunTest

-call runtest.bat -nologo -logPrefix:%1 %2 %3 %4 %5 %6 %7 %8 %9 > Output

+call runtest.bat -nologo -logPrefix:%* > Output

 rem There seem to be some race between finishing writing to the Output file, and running fc.

 rem Calling fc twice seems to fix (or at least alleviate) the problem.

 fc /W Answer Output > nul