From aff91f102b21cddf725a730f32526c2f7b418d54 Mon Sep 17 00:00:00 2001
From: mkawa <unknown>
Date: Wed, 23 Sep 2009 21:12:17 +0000
Subject: Added /z3multipleErrors flag for generation of multiple
 counterexamples per assert (switches off z3's /@ flag).

---
 Source/Core/CommandLineOptions.ssc | 7 +++++++
 Source/Provers/Z3/Prover.ssc       | 8 +++++---
 2 files changed, 12 insertions(+), 3 deletions(-)

(limited to 'Source')

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;
-- 
cgit v1.2.3