diff options
Diffstat (limited to 'Source/Provers/SMTLib/ProverInterface.cs')
-rw-r--r-- | Source/Provers/SMTLib/ProverInterface.cs | 13 |
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);
|