diff options
author | 2011-11-11 14:19:32 +0530 | |
---|---|---|
committer | 2011-11-11 14:19:32 +0530 | |
commit | 809c36440c2ddc753fcd7397c492aba21182321c (patch) | |
tree | 66fb2e907ef496f406f7ae647cba69b2f65c6f7c | |
parent | 277d5007f1b5d6988014d758e7ca1a486e1c6395 (diff) |
Produce unsat cores only when enabled (in stratified inlining)
-rw-r--r-- | Source/Provers/SMTLib/ProverInterface.cs | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index 0c9a7513..d3448b5d 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -27,6 +27,7 @@ namespace Microsoft.Boogie.SMTLib private readonly SMTLibProverContext ctx;
private readonly VCExpressionGenerator gen;
private readonly SMTLibProverOptions options;
+ private bool usingUnsatCore;
[ContractInvariantMethod]
void ObjectInvariant()
@@ -54,6 +55,7 @@ namespace Microsoft.Boogie.SMTLib this.options = (SMTLibProverOptions)options;
this.ctx = ctx;
this.gen = gen;
+ this.usingUnsatCore = false;
TypeAxiomBuilder axBuilder;
switch (CommandLineOptions.Clo.TypeEncodingMethod) {
@@ -84,7 +86,11 @@ namespace Microsoft.Boogie.SMTLib {
currentLogFile = OpenOutputFile("");
}
- SendThisVC("(set-option :produce-unsat-cores true)");
+ if (CommandLineOptions.Clo.ProcedureCopyBound > 0 || CommandLineOptions.Clo.UseUnsatCoreForInlining)
+ {
+ SendThisVC("(set-option :produce-unsat-cores true)");
+ this.usingUnsatCore = true;
+ }
PrepareCommon();
}
prevOutcomeAvailable = false;
@@ -781,7 +787,7 @@ namespace Microsoft.Boogie.SMTLib pendingPop = true;
return;
}
-
+ Contract.Assert(usingUnsatCore, "SMTLib prover not setup for computing unsat cores");
SendThisVC("(get-unsat-core)");
var resp = Process.GetProverResponse();
unsatCore = new List<int>();
|