diff options
| author |  mkawa <unknown> | 2009-09-23 21:12:17 +0000 |
|---|---|---|
| committer | mkawa <unknown> | 2009-09-23 21:12:17 +0000 |
| commit | aff91f102b21cddf725a730f32526c2f7b418d54 (patch) | |
| tree | 3540a257ec984f43ad80b0d5f83cd0422ca98577 /Source/Provers | |
| parent | 7d9a1e78eb07f592065a69db862d92014d5c1894 (diff) | |
Added /z3multipleErrors flag for generation of multiple counterexamples per assert (switches off z3's /@ flag).
Diffstat (limited to 'Source/Provers')
| -rw-r--r-- | Source/Provers/Z3/Prover.ssc | 8 |
1 files changed, 5 insertions, 3 deletions
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;
|