Disable MBQI and AUTO_CONFIG

1 files changed, 6 insertions, 0 deletions

diff --git a/Source/Provers/SMTLib/Z3.cs b/Source/Provers/SMTLib/Z3.cs
index feb8b109..f0801b22 100644
--- a/Source/Provers/SMTLib/Z3.cs
+++ b/Source/Provers/SMTLib/Z3.cs
@@ -104,6 +104,9 @@ namespace Microsoft.Boogie.SMTLib
 

     public static void SetupOptions(SMTLibProverOptions options)

     {

+      // 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.WeakAddSmtOption("MODEL_VALUE_COMPLETION", "false");

       options.AddWeakSmtOption("MODEL_HIDE_UNUSED_PARTITIONS", "false");

@@ -133,6 +136,9 @@ namespace Microsoft.Boogie.SMTLib
       // the foo(x0) will be activated for e-matching when x is skolemized to x0.

       options.AddWeakSmtOption("NNF_SK_HACK", "true");

 

+      // don't use model-based quantifier instantiation; it never finishes on non-trivial Boogie problems

+      options.AddWeakSmtOption("MBQI", "false");      

+

       // More or less like MAM=0.

       options.AddWeakSmtOption("QI_EAGER_THRESHOLD", "100");

       // Complex proof attempts in VCC (and likely elsewhere) require matching depth of 20 or more.