Merge

9 files changed, 23 insertions, 50 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/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/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/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