diff options
| author |  qadeer <qadeer@microsoft.com> | 2012-04-01 22:21:52 -0700 |
|---|---|---|
| committer | qadeer <qadeer@microsoft.com> | 2012-04-01 22:21:52 -0700 |
| commit | bc42f101e4389d954afadae0e9fe95f7acc6c4ad (patch) | |
| tree | 029597ed22aaa6b8e84829b83b4b02c6ac73c195 /Source | |
| parent | 3968dee28a8ee0c7164fb98208a796657c3b8479 (diff) | |
| parent | 4ab395733bd4208651ac3edb2fe06f3170201986 (diff) | |
Merge
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Provers/SMTLib/ProverInterface.cs | 4 | ||||
| -rw-r--r-- | Source/VCGeneration/Check.cs | 4 | ||||
| -rw-r--r-- | Source/VCGeneration/StratifiedVC.cs | 2 |
3 files changed, 5 insertions, 5 deletions
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index 6ba49a8f..5e262f87 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -792,7 +792,7 @@ namespace Microsoft.Boogie.SMTLib /// </summary>
static int nameCounter = 0;
- public override Outcome CheckAssumptions(List<VCExpr> assumptions, out List<int> unsatCore)
+ public override Outcome CheckAssumptions(List<VCExpr> assumptions, out List<int> unsatCore, ErrorHandler handler)
{
unsatCore = new List<int>();
@@ -810,7 +810,7 @@ namespace Microsoft.Boogie.SMTLib }
Check();
- var prevOutcome = GetResponse();
+ var prevOutcome = CheckOutcomeCore(handler);
if (prevOutcome != Outcome.Valid)
{
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs index 832d4430..1a6732c2 100644 --- a/Source/VCGeneration/Check.cs +++ b/Source/VCGeneration/Check.cs @@ -823,8 +823,8 @@ namespace Microsoft.Boogie { throw new NotImplementedException();
}
- // (check-sat + get-unsat-core)
- public virtual Outcome CheckAssumptions(List<VCExpr> assumptions, out List<int> unsatCore)
+ // (check-sat + get-unsat-core + checkOutcome)
+ public virtual Outcome CheckAssumptions(List<VCExpr> assumptions, out List<int> unsatCore, ErrorHandler handler)
{
throw new NotImplementedException();
}
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index 965939fc..b9ab40b2 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -1161,7 +1161,7 @@ namespace VC TheoremProver.Push();
TheoremProver.AssertAxioms();
- ProverInterface.Outcome outcome = TheoremProver.CheckAssumptions(assumptions, out unsatCore);
+ ProverInterface.Outcome outcome = TheoremProver.CheckAssumptions(assumptions, out unsatCore, reporter);
TheoremProver.Pop();
numQueries++;
|