diff options
Diffstat (limited to 'Source/Provers')
| -rw-r--r-- | Source/Provers/SMTLib/ProverInterface.cs | 7 | ||||
| -rw-r--r-- | Source/Provers/SMTLib/Z3.cs | 2 |
2 files changed, 3 insertions, 6 deletions
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index f1a00873..5efbb96f 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -435,10 +435,7 @@ namespace Microsoft.Boogie.SMTLib }
if (wasUnknown) {
- if (options.UseZ3)
- SendThisVC("(get-info :last-failure)");
- else
- SendThisVC("(get-info :reason-unknown)");
+ SendThisVC("(get-info :reason-unknown)");
Process.Ping();
while (true) {
@@ -446,7 +443,7 @@ namespace Microsoft.Boogie.SMTLib if (resp == null || Process.IsPong(resp))
break;
- if (resp.ArgCount == 1 && (resp.Name == ":reason-unknown" || resp.Name == ":last-failure")) {
+ if (resp.ArgCount == 1 && resp.Name == ":reason-unknown") {
switch (resp[0].Name) {
case "memout":
result = Outcome.OutOfMemory;
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.
|