summaryrefslogtreecommitdiff
path: root/Source/Provers/SMTLib/ProverInterface.cs
diff options
context:
space:
mode:
authorGravatar shuvendu <unknown>2014-11-07 16:40:29 -0800
committerGravatar shuvendu <unknown>2014-11-07 16:40:29 -0800
commit8bd30420a8c0ee31137b37e288b7ef69e181f3ab (patch)
tree4a0988960c2a081bab9fbfcd4e9eeb7259cf5731 /Source/Provers/SMTLib/ProverInterface.cs
parent98c24910e7e01d7748930743548431a203e2be24 (diff)
re-enabling -useUnsatCoreForContractInfer
An example houdini\testUnsatCore.bpl to test out the unsatCore (Currently seems to be not working)
Diffstat (limited to 'Source/Provers/SMTLib/ProverInterface.cs')
-rw-r--r--Source/Provers/SMTLib/ProverInterface.cs2
1 files changed, 1 insertions, 1 deletions
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index ece49e23..fc2b25f1 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -81,7 +81,7 @@ namespace Microsoft.Boogie.SMTLib
{
currentLogFile = OpenOutputFile("");
}
- if (CommandLineOptions.Clo.ContractInfer && CommandLineOptions.Clo.ExplainHoudini)
+ if (CommandLineOptions.Clo.ContractInfer && (CommandLineOptions.Clo.UseUnsatCoreForContractInfer || CommandLineOptions.Clo.ExplainHoudini))
{
SendThisVC("(set-option :produce-unsat-cores true)");
this.usingUnsatCore = true;