diff options
| author |  Michal Moskal <michal@moskal.me> | 2012-02-28 12:00:09 -0800 |
|---|---|---|
| committer | Michal Moskal <michal@moskal.me> | 2012-02-28 12:00:09 -0800 |
| commit | d844df2d9a79b14a1f4b1337c4bbcd56e241d4d4 (patch) | |
| tree | b8e5d4040251242504eec51a78c4eec301a08ca4 /Source/VCGeneration/Check.cs | |
| parent | 7c3d836e67c3205b7d306529b87e26fe9e4d75bd (diff) | |
Introduce ApiProverInterface.CheckOutcomeCore() for stratified inlining; simplify push/pop handling
Diffstat (limited to 'Source/VCGeneration/Check.cs')
| -rw-r--r-- | Source/VCGeneration/Check.cs | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs index 5176d494..f0e6b384 100644 --- a/Source/VCGeneration/Check.cs +++ b/Source/VCGeneration/Check.cs @@ -848,6 +848,7 @@ namespace Microsoft.Boogie { public abstract void AssertAxioms();
public abstract void Check();
public abstract void CheckAssumptions(List<VCExpr> assumptions, out List<int> unsatCore);
+ public abstract Outcome CheckOutcomeCore(ErrorHandler handler);
public abstract void Push();
public virtual void SetTimeOut(int ms) { }
}
|