diff options
| author |  Michal Moskal <michal@moskal.me> | 2011-04-28 10:43:13 -0700 |
|---|---|---|
| committer | Michal Moskal <michal@moskal.me> | 2011-04-28 10:43:13 -0700 |
| commit | 19119542222cb54869e6bd691ed77667838743e2 (patch) | |
| tree | 923dd54c5e92f5f292293cfca6dc3b39ac1e3cf0 /Source/Provers/SMTLib/Z3.cs | |
| parent | cf4b94200784ee111fef7c97826a96ffeb9bd1cb (diff) | |
Use :reason-unknown not :last-failure for Z3 in SMT mode; disable SORT_AND_OR option (obsolete)
Diffstat (limited to 'Source/Provers/SMTLib/Z3.cs')
| -rw-r--r-- | Source/Provers/SMTLib/Z3.cs | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Source/Provers/SMTLib/Z3.cs b/Source/Provers/SMTLib/Z3.cs index 27d86915..54742802 100644 --- a/Source/Provers/SMTLib/Z3.cs +++ b/Source/Provers/SMTLib/Z3.cs @@ -124,7 +124,7 @@ namespace Microsoft.Boogie.SMTLib options.AddWeakSmtOption("ARITH_RANDOM_INITIAL_VALUE", "true");
// The left-to-right structural case-splitting strategy.
- options.AddWeakSmtOption("SORT_AND_OR", "false");
+ //options.AddWeakSmtOption("SORT_AND_OR", "false"); // always false now
options.AddWeakSmtOption("CASE_SPLIT", "3");
// In addition delay adding unit conflicts.
|