diff options
| author |  qadeer <qadeer@microsoft.com> | 2012-04-01 21:39:57 -0700 |
|---|---|---|
| committer | qadeer <qadeer@microsoft.com> | 2012-04-01 21:39:57 -0700 |
| commit | cfbb83ff12549044fa0ed9e143ee0a54fcef24d5 (patch) | |
| tree | 542deba017b611484b6d19dc4621ddb3b65738ec /Source/VCGeneration/Check.cs | |
| parent | 47d399289a1d36c9473f145fb1e63e6db3420128 (diff) | |
partial work on non-uniform loop unrolling
Diffstat (limited to 'Source/VCGeneration/Check.cs')
| -rw-r--r-- | Source/VCGeneration/Check.cs | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs index d74497c0..5702111d 100644 --- a/Source/VCGeneration/Check.cs +++ b/Source/VCGeneration/Check.cs @@ -829,6 +829,10 @@ namespace Microsoft.Boogie { throw new NotImplementedException();
}
+ public virtual Outcome CheckAssumptions(List<VCExpr> hardAssumptions, List<VCExpr> softAssumptions, out List<int> unsatisfiedSoftAssumptions) {
+ throw new NotImplementedException();
+ }
+
public virtual Outcome CheckOutcomeCore(ErrorHandler handler)
{
throw new NotImplementedException();
|