diff options
author | Ken McMillan <unknown> | 2014-05-26 14:36:26 -0700 |
---|---|---|
committer | Ken McMillan <unknown> | 2014-05-26 14:36:26 -0700 |
commit | 137f285e5a45d5e4ce3eaa40fc68df7890a3d2d7 (patch) | |
tree | 1c6456d6f1a52193f59e9a06b4835ff746b637ba /Source/Provers/SMTLib/Z3.cs | |
parent | c86d9a5a06cfe53ce070cb78abe89b1747bb7769 (diff) | |
parent | 7d9165d6b61e7475b973d3bf86d063dcc4a454d1 (diff) |
Merge duality changes
Diffstat (limited to 'Source/Provers/SMTLib/Z3.cs')
-rw-r--r-- | Source/Provers/SMTLib/Z3.cs | 16 |
1 files changed, 13 insertions, 3 deletions
diff --git a/Source/Provers/SMTLib/Z3.cs b/Source/Provers/SMTLib/Z3.cs index 63c95afe..fce83b63 100644 --- a/Source/Provers/SMTLib/Z3.cs +++ b/Source/Provers/SMTLib/Z3.cs @@ -4,6 +4,7 @@ //
//-----------------------------------------------------------------------------
+
using System;
using System.Collections.Generic;
using System.Linq;
@@ -187,6 +188,7 @@ namespace Microsoft.Boogie.SMTLib // options that work only on the command line
static string[] commandLineOnly = { "TRACE", "PROOF_MODE" };
+
public static void SetupOptions(SMTLibProverOptions options)
{
FindExecutable();
@@ -195,8 +197,10 @@ namespace Microsoft.Boogie.SMTLib if (major > 4 || major == 4 && minor >= 3)
{
+ bool fp = false; // CommandLineOptions.Clo.FixedPointEngine != null;
+
// don't bother with auto-config - it would disable explicit settings for eager threshold and so on
- options.AddWeakSmtOption("AUTO_CONFIG", "false");
+ if(!fp) options.AddWeakSmtOption("AUTO_CONFIG", "false");
//options.AddWeakSmtOption("MODEL_PARTIAL", "true");
//options.WeakAddSmtOption("MODEL_VALUE_COMPLETION", "false");
@@ -219,7 +223,8 @@ namespace Microsoft.Boogie.SMTLib // The left-to-right structural case-splitting strategy.
//options.AddWeakSmtOption("SORT_AND_OR", "false"); // always false now
- options.AddWeakSmtOption("smt.CASE_SPLIT", "3");
+
+ if (!fp) options.AddWeakSmtOption("smt.CASE_SPLIT", "3");
// In addition delay adding unit conflicts.
options.AddWeakSmtOption("smt.DELAY_UNITS", "true");
@@ -238,7 +243,7 @@ namespace Microsoft.Boogie.SMTLib // Complex proof attempts in VCC (and likely elsewhere) require matching depth of 20 or more.
// the following will make the :weight option more usable
- options.AddWeakSmtOption("smt.QI.COST", "|\"(+ weight generation)\"|"); // TODO: this doesn't seem to work
+ if (!fp) options.AddWeakSmtOption("smt.QI.COST", "|\"(+ weight generation)\"|"); // TODO: this doesn't seem to work
//if (options.Inspector != null)
// options.WeakAddSmtOption("PROGRESS_SAMPLING_FREQ", "100");
@@ -262,6 +267,11 @@ namespace Microsoft.Boogie.SMTLib options.AddWeakSmtOption("smt.array.weak", "true");
options.AddWeakSmtOption("smt.array.extensional", "false");
}
+
+ if (CommandLineOptions.Clo.PrintConjectures != null)
+ {
+ options.AddWeakSmtOption("fixedpoint.conjecture_file", CommandLineOptions.Clo.PrintConjectures + ".tmp");
+ }
}
else
{
|