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/Provers/Z3/Prover.ssc | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'Source/Provers/Z3')

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