diff options
| author |  Rustan Leino <unknown> | 2013-08-02 19:55:08 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2013-08-02 19:55:08 -0700 |
| commit | d5a32ffd75e5723a5f2a6f9d6a5b50b3e692a0ff (patch) | |
| tree | 515467998879453d6d49e02136bfaa55537d7179 /Source/Provers/SMTLib/Z3.cs | |
| parent | a8d8cda9bc77e63c2bf4e14b5b5928ce43e75547 (diff) | |
Reverted change to use MODEL_ON_FINAL_CHECK, which seems to cause Z3 unexpectedly to output model information
Diffstat (limited to 'Source/Provers/SMTLib/Z3.cs')
| -rw-r--r-- | Source/Provers/SMTLib/Z3.cs | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/Source/Provers/SMTLib/Z3.cs b/Source/Provers/SMTLib/Z3.cs index 14b8ebb2..a2bf80ba 100644 --- a/Source/Provers/SMTLib/Z3.cs +++ b/Source/Provers/SMTLib/Z3.cs @@ -352,7 +352,6 @@ namespace Microsoft.Boogie.SMTLib }
options.AddWeakSmtOption("MODEL_ON_TIMEOUT", "true");
- options.AddWeakSmtOption("MODEL_ON_FINAL_CHECK", "true");
// legacy option handling
if (!CommandLineOptions.Clo.z3AtFlag)
|