diff options
| author |  Dan Liew <daniel.liew@imperial.ac.uk> | 2014-09-19 13:36:18 +0100 |
|---|---|---|
| committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2014-09-19 13:36:18 +0100 |
| commit | ac31d6bb389e4db49f268bf39c644fec2411ce67 (patch) | |
| tree | bdf320713be7bd9a61312ac7229e9683fd4004f0 /Source/Provers | |
| parent | f909bceb37a15c2a99668aa56dfefc321cff074a (diff) | |
Patch by Jeroen Ketema.
Only set produce-unsat-cores in the case /explainHoudini is passed. This
allows contract inference to be used with solvers that do no support unsat
cores, as long as no explanation of the Houdini run is required.
Diffstat (limited to 'Source/Provers')
| -rw-r--r-- | Source/Provers/SMTLib/ProverInterface.cs | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index fd7c1bda..6b8e03d1 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -81,14 +81,13 @@ namespace Microsoft.Boogie.SMTLib {
currentLogFile = OpenOutputFile("");
}
- if (CommandLineOptions.Clo.ContractInfer)
+ if (CommandLineOptions.Clo.ContractInfer && CommandLineOptions.Clo.ExplainHoudini)
{
SendThisVC("(set-option :produce-unsat-cores true)");
this.usingUnsatCore = true;
}
PrepareCommon();
}
-
}
private void SetupAxiomBuilder(VCExpressionGenerator gen)
|