summaryrefslogtreecommitdiff
path: root/Source/Provers/SMTLib/Z3.cs
diff options
context:
space:
mode:
authorGravatar MichalMoskal <unknown>2011-02-23 00:49:17 +0000
committerGravatar MichalMoskal <unknown>2011-02-23 00:49:17 +0000
commita725d481d41980c800fbe8e1643812d09a77cde0 (patch)
tree47dd911b39b214e3cd53de34e7a6c9b4eca27397 /Source/Provers/SMTLib/Z3.cs
parentb97dc01fb8dec7f266c2e0fd8a4e96df0f14c5d7 (diff)
Parse else-> clauses in the model
Disable MODEL_PARTIAL in SMTLib
Diffstat (limited to 'Source/Provers/SMTLib/Z3.cs')
-rw-r--r--Source/Provers/SMTLib/Z3.cs2
1 files changed, 1 insertions, 1 deletions
diff --git a/Source/Provers/SMTLib/Z3.cs b/Source/Provers/SMTLib/Z3.cs
index 8b21861e..80a220cb 100644
--- a/Source/Provers/SMTLib/Z3.cs
+++ b/Source/Provers/SMTLib/Z3.cs
@@ -107,7 +107,7 @@ namespace Microsoft.Boogie.SMTLib
// don't bother with auto-config - it would disable explicit settings for eager threshold and so on
options.AddWeakSmtOption("AUTO_CONFIG", "false");
- options.AddWeakSmtOption("MODEL_PARTIAL", "true");
+ //options.AddWeakSmtOption("MODEL_PARTIAL", "true");
//options.WeakAddSmtOption("MODEL_VALUE_COMPLETION", "false");
options.AddWeakSmtOption("MODEL_HIDE_UNUSED_PARTITIONS", "false");
options.AddWeakSmtOption("MODEL_V2", "true");