diff options
| author |  MichalMoskal <unknown> | 2011-02-21 21:54:01 +0000 |
|---|---|---|
| committer | MichalMoskal <unknown> | 2011-02-21 21:54:01 +0000 |
| commit | cc31c5d516332f1a70f88f4113d69e8987883589 (patch) | |
| tree | 2d94886636a1cd7ab27213a8b53c13ba4842483a /Source/Provers | |
| parent | a8ca55329e361d28cd2bebc9a6ce06145cb3e4e4 (diff) | |
Allow recent Z3 versions to be used
Diffstat (limited to 'Source/Provers')
| -rw-r--r-- | Source/Provers/Z3/Prover.cs | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/Source/Provers/Z3/Prover.cs b/Source/Provers/Z3/Prover.cs index 81fa61a2..c2bb7500 100644 --- a/Source/Provers/Z3/Prover.cs +++ b/Source/Provers/Z3/Prover.cs @@ -3,6 +3,9 @@ // Copyright (C) Microsoft Corporation. All Rights Reserved.
//
//-----------------------------------------------------------------------------
+
+//#define RECENT_Z3 // 2.20 or newer
+
using System;
using System.IO;
using System.Diagnostics;
@@ -109,11 +112,18 @@ namespace Microsoft.Boogie.Z3 List<OptionValue/*!*/>/*!*/ result = new List<OptionValue/*!*/>();
AddOption(result, "MODEL_PARTIAL", "true");
- AddOption(result, "MODEL_VALUE_COMPLETION", "false");
+
AddOption(result, "MODEL_HIDE_UNUSED_PARTITIONS", "false");
AddOption(result, "MODEL_V1", "true");
AddOption(result, "ASYNC_COMMANDS", "false");
+#if RECENT_Z3
+ AddOption(result, "AUTO_CONFIG", "false");
+ AddOption(result, "MBQI", "false");
+#else
+ AddOption(result, "MODEL_VALUE_COMPLETION", "false");
+#endif
+
if (!opts.OptimizeForBv) {
// Phase selection means to always try the negative literal polarity first, seems to be good for Boogie.
// The restart parameters change the restart behavior to match Z3 v1, which also seems to be good.
|