diff options
| author |  Akash Lal <akashl@microsoft.com> | 2015-05-13 14:33:48 +0530 |
|---|---|---|
| committer | Akash Lal <akashl@microsoft.com> | 2015-05-13 14:33:48 +0530 |
| commit | d4d66e2ad626eb1539e2b3e3aa0e88ad6b7746aa (patch) | |
| tree | 4fa33ce1e0fc6fdea1c29442343d1094b89b9580 /Source/VCGeneration/FixedpointVC.cs | |
| parent | 86b45ab19c90f6759f5685b1616961e1400fa4ba (diff) | |
Fix for printFixedPoint when dealing with functions
Diffstat (limited to 'Source/VCGeneration/FixedpointVC.cs')
| -rw-r--r-- | Source/VCGeneration/FixedpointVC.cs | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/Source/VCGeneration/FixedpointVC.cs b/Source/VCGeneration/FixedpointVC.cs index 7dbf6b05..5c698633 100644 --- a/Source/VCGeneration/FixedpointVC.cs +++ b/Source/VCGeneration/FixedpointVC.cs @@ -2189,7 +2189,13 @@ namespace Microsoft.Boogie idx.Add(args[1]);
return Expr.Store(args[0],idx,args[2]);
}
-
+
+ if (f.Op is VCExprBoogieFunctionOp)
+ {
+ return new NAryExpr(Token.NoToken,
+ new FunctionCall((f.Op as VCExprBoogieFunctionOp).Func), args);
+ }
+
var op = VCOpToOp (f.Op);
return MakeBinary(op,args);
}
|