diff options
Diffstat (limited to 'Source/VCGeneration/Check.cs')
| -rw-r--r-- | Source/VCGeneration/Check.cs | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs index f9999a74..9ebf4d63 100644 --- a/Source/VCGeneration/Check.cs +++ b/Source/VCGeneration/Check.cs @@ -851,9 +851,14 @@ namespace Microsoft.Boogie { public abstract ProverContext Context {
get;
}
+
public abstract VCExpressionGenerator VCExprGen {
get;
}
+
+ public virtual void DefineMacro(Function fun, VCExpr vc) {
+ throw new NotImplementedException();
+ }
}
public class ProverInterfaceContracts : ProverInterface {
|