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

1 files changed, 7 insertions, 0 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