diff options
| author |  Pantazis Deligiannis <pdeligia@me.com> | 2013-07-19 11:03:54 +0100 |
|---|---|---|
| committer | Pantazis Deligiannis <pdeligia@me.com> | 2013-07-19 11:03:54 +0100 |
| commit | 2c4fff7b78774a98525e475e8a4e078ecf94583d (patch) | |
| tree | a4771f0a20fcc23ea35be3ccdd79eb979d01414f /Source/Provers/SMTLib/Z3.cs | |
| parent | cf4543349ed64553d9d5a07a8d238a80a913eebb (diff) | |
refactoring and fixes in the SMTLIB2 parser
Diffstat (limited to 'Source/Provers/SMTLib/Z3.cs')
| -rw-r--r-- | Source/Provers/SMTLib/Z3.cs | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/Source/Provers/SMTLib/Z3.cs b/Source/Provers/SMTLib/Z3.cs index 5865a333..d2e06168 100644 --- a/Source/Provers/SMTLib/Z3.cs +++ b/Source/Provers/SMTLib/Z3.cs @@ -285,12 +285,9 @@ namespace Microsoft.Boogie.SMTLib options.AddWeakSmtOption("MODEL_HIDE_UNUSED_PARTITIONS", "false");
options.AddWeakSmtOption("ASYNC_COMMANDS", "false");
- if (options.SMTLib2Model)
- {
+ if (CommandLineOptions.Clo.UseSmtOutputFormat) {
options.AddWeakSmtOption("pp-bv-literals", "false");;
- }
- else
- {
+ } else {
options.AddWeakSmtOption("MODEL_V2", "true");
}
|