Added /z3multipleErrors flag for generation of multiple counterexamples per assert (switches off z3's /@ flag).

2 files changed, 12 insertions, 3 deletions

diff --git a/Source/Core/CommandLineOptions.ssc b/Source/Core/CommandLineOptions.ssc
index 244dc640..952bad92 100644
--- a/Source/Core/CommandLineOptions.ssc
+++ b/Source/Core/CommandLineOptions.ssc
@@ -171,6 +171,7 @@ namespace Microsoft.Boogie
     public int ProverKillTime = -1;  // -1 means not specified

     public int SmokeTimeout = 10; // default to 10s

     public int ProverCCLimit = 5;

+    public bool z3AtFlag = true;

     public bool RestartProverPerVC = false; 

 

     public double VcsMaxCost = 1.0;

@@ -1020,6 +1021,11 @@ namespace Microsoft.Boogie
             ps.GetNumericArgument(ref ProverCCLimit);

             break;

             

+          case "-z3multipleErrors":

+          case "/z3multipleErrors":

+            z3AtFlag = false;

+            break;

+            

           case "-z3mam":

           case "/z3mam":

           {

@@ -1944,6 +1950,7 @@ namespace Microsoft.Boogie
   /z3opt:<arg>   : specify additional Z3 options

   /z3DebugTrace:<arg>   : z3 command line options so that Z3 generates debug

                    tracing

+  /z3multipleErrors : report multiple counterexamples for each error

 

   SMT-Lib specific options:

   /smtOutput:<file>     : Path and basename to which the prover output is

diff --git a/Source/Provers/Z3/Prover.ssc b/Source/Provers/Z3/Prover.ssc
index 13c71814..3fbb8a4a 100644
--- a/Source/Provers/Z3/Prover.ssc
+++ b/Source/Provers/Z3/Prover.ssc
@@ -89,10 +89,12 @@ namespace Microsoft.Boogie.Z3
       } else {

         z3args += " " + OptionChar() + "mam:" + CommandLineOptions.Clo.Z3mam;

       }

-

+      

+      if (CommandLineOptions.Clo.z3AtFlag) {

+		z3args += " " + OptionChar() + "@ ";

+	  }

       if (0 <= CommandLineOptions.Clo.ProverCCLimit) {

-        z3args += " " + OptionChar() + "@ " +

-                        OptionChar() + "cex:" + CommandLineOptions.Clo.ProverCCLimit;

+        z3args += " " + OptionChar() + "cex:" + CommandLineOptions.Clo.ProverCCLimit;

       }

       if (0 <= opts.Timeout) {

         z3args += " " + OptionChar() + "t:" + opts.Timeout;