From 19119542222cb54869e6bd691ed77667838743e2 Mon Sep 17 00:00:00 2001 From: Michal Moskal Date: Thu, 28 Apr 2011 10:43:13 -0700 Subject: Use :reason-unknown not :last-failure for Z3 in SMT mode; disable SORT_AND_OR option (obsolete) --- Source/Provers/SMTLib/ProverInterface.cs | 7 ++----- Source/Provers/SMTLib/Z3.cs | 2 +- 2 files changed, 3 insertions(+), 6 deletions(-) (limited to 'Source/Provers') 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. -- cgit v1.2.3