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 +++++++
 1 file changed, 7 insertions(+)

(limited to 'Source/Core')

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