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);