diff options
| author |  pantazis <pdeligia@me.com> | 2013-06-12 11:56:12 +0100 |
|---|---|---|
| committer | pantazis <pdeligia@me.com> | 2013-06-12 11:56:12 +0100 |
| commit | afa66db65a59b45960ffa172cfcb628a67a97177 (patch) | |
| tree | 1741bc3011e0a77345eeae153ae9e734b9448837 /Source/Provers/SMTLib/Z3.cs | |
| parent | 62358a4e290dca623f0af0bba72eeda6ec6dcaa2 (diff) | |
Z3 new parser takes now a new option for pp-bv-literals
Diffstat (limited to 'Source/Provers/SMTLib/Z3.cs')
| -rw-r--r-- | Source/Provers/SMTLib/Z3.cs | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/Source/Provers/SMTLib/Z3.cs b/Source/Provers/SMTLib/Z3.cs index 81d5d5d1..04bdc0df 100644 --- a/Source/Provers/SMTLib/Z3.cs +++ b/Source/Provers/SMTLib/Z3.cs @@ -274,7 +274,8 @@ namespace Microsoft.Boogie.SMTLib //options.AddWeakSmtOption("MODEL_PARTIAL", "true");
//options.WeakAddSmtOption("MODEL_VALUE_COMPLETION", "false");
options.AddWeakSmtOption("MODEL_HIDE_UNUSED_PARTITIONS", "false");
- options.AddWeakSmtOption("MODEL_V2", "true");
+ //options.AddWeakSmtOption("MODEL_V2", "true");
+ options.AddWeakSmtOption("pp-bv-literals", "false");
options.AddWeakSmtOption("ASYNC_COMMANDS", "false");
if (!options.OptimizeForBv)
|