diff options
Diffstat (limited to 'Source/VCGeneration/ExprExtensions.cs')
| -rw-r--r-- | Source/VCGeneration/ExprExtensions.cs | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/Source/VCGeneration/ExprExtensions.cs b/Source/VCGeneration/ExprExtensions.cs index 67837833..e242257f 100644 --- a/Source/VCGeneration/ExprExtensions.cs +++ b/Source/VCGeneration/ExprExtensions.cs @@ -139,10 +139,29 @@ namespace Microsoft.Boogie.ExprExtensions return Function(f, args);
}
+ public Term MkApp(FuncDecl f, Term[] args, Type[]/*!*/ typeArguments)
+ {
+ return Function(f, args, typeArguments);
+ }
+
public Term MkApp(FuncDecl f, Term arg)
{
return Function(f, arg);
}
+
+ public Term CloneApp(Term t, Term[] args)
+ {
+ var f = t.GetAppDecl();
+ var typeArgs = (t as VCExprNAry).TypeArguments;
+ if (typeArgs != null && typeArgs.Count > 0)
+ {
+ return MkApp(f, args, typeArgs.ToArray());
+ }
+ else
+ {
+ return MkApp(f, args);
+ }
+ }
public Term MkAnd(Term[] args)
{
|