diff options
| author |  wuestholz <unknown> | 2014-11-05 10:33:09 +0100 |
|---|---|---|
| committer | wuestholz <unknown> | 2014-11-05 10:33:09 +0100 |
| commit | 9a133cbc803272f38ea7d93dc4b295940bf05c8d (patch) | |
| tree | 2433a9caf1691502e1282cf1ca149210251d2e60 /Source/Provers/SMTLib/Z3.cs | |
| parent | 5b4c25763d3d5fff4c034770a31f2a7dd3508167 (diff) | |
Minor change to make some regression tests work with Z3 4.3.2
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 fce83b63..a0d6ba86 100644 --- a/Source/Provers/SMTLib/Z3.cs +++ b/Source/Provers/SMTLib/Z3.cs @@ -243,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
- if (!fp) 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");
|