Work around bug in Z3 4.3.2 and newer (https://z3.codeplex.com/workitem/188)

where setting produce-unsat-cores to true has no effect unless the option is set last.

This makes the Test/houdini/testUnsatCore.bpl test pass under Linux using Z3 4.3.2

1 files changed, 8 insertions, 5 deletions

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index 320d0469..15bb3257 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -81,11 +81,6 @@ namespace Microsoft.Boogie.SMTLib
           {

               currentLogFile = OpenOutputFile("");

           }

-          if (CommandLineOptions.Clo.ContractInfer && (CommandLineOptions.Clo.UseUnsatCoreForContractInfer || CommandLineOptions.Clo.ExplainHoudini))

-          {

-              SendThisVC("(set-option :produce-unsat-cores true)");

-              this.usingUnsatCore = true;

-          }

           PrepareCommon();

       }

     }

@@ -246,6 +241,14 @@ namespace Microsoft.Boogie.SMTLib
           SendCommon("(set-logic " + options.Logic + ")");

         }

 

+        // Set produce-unsat-cores last. It seems there's a bug in Z3 where if we set it earlier its value

+        // gets reset by other set-option commands ( https://z3.codeplex.com/workitem/188 )

+        if (CommandLineOptions.Clo.ContractInfer && (CommandLineOptions.Clo.UseUnsatCoreForContractInfer || CommandLineOptions.Clo.ExplainHoudini))

+        {

+          SendThisVC("(set-option :produce-unsat-cores true)");

+          this.usingUnsatCore = true;

+        }

+

         SendCommon("; done setting options\n");

         SendCommon(_backgroundPredicates);