diff options
| author |  Pantazis Deligiannis <pdeligia@me.com> | 2013-07-09 22:12:51 +0100 |
|---|---|---|
| committer | Pantazis Deligiannis <pdeligia@me.com> | 2013-07-09 22:12:51 +0100 |
| commit | 0ad93c637c97672fa71c380f9112ea1b7d6572d8 (patch) | |
| tree | 81796eee129a7763e3930c3da31c5b4c4aaac5b0 /Source/Provers/SMTLib/Z3.cs | |
| parent | e8e4c58f700242eab9e951e01c8a2ee3cafd89de (diff) | |
added specific command line options to enable the SMTLIB2 output model parser for Z3. Use /proverOpt:SMTLIB2_MODEL=true
Diffstat (limited to 'Source/Provers/SMTLib/Z3.cs')
| -rw-r--r-- | Source/Provers/SMTLib/Z3.cs | 11 |
1 files changed, 9 insertions, 2 deletions
diff --git a/Source/Provers/SMTLib/Z3.cs b/Source/Provers/SMTLib/Z3.cs index 66b1809a..5865a333 100644 --- a/Source/Provers/SMTLib/Z3.cs +++ b/Source/Provers/SMTLib/Z3.cs @@ -283,10 +283,17 @@ 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("pp-bv-literals", "false");
options.AddWeakSmtOption("ASYNC_COMMANDS", "false");
+ if (options.SMTLib2Model)
+ {
+ options.AddWeakSmtOption("pp-bv-literals", "false");;
+ }
+ else
+ {
+ options.AddWeakSmtOption("MODEL_V2", "true");
+ }
+
if (!options.OptimizeForBv)
{
// Phase selection means to always try the negative literal polarity first, seems to be good for Boogie.
|