diff options
| -rw-r--r-- | Source/Provers/SMTLib/TypeDeclCollector.cs | 1 | ||||
| -rw-r--r-- | Source/VCGeneration/FixedpointVC.cs | 8 |
2 files changed, 8 insertions, 1 deletions
diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs index 30363102..9205d54c 100644 --- a/Source/Provers/SMTLib/TypeDeclCollector.cs +++ b/Source/Provers/SMTLib/TypeDeclCollector.cs @@ -231,6 +231,7 @@ void ObjectInvariant() else
decl = "(declare-fun " + printedName + " (" + argTypes + ") " + TypeToStringReg(f.OutParams[0].TypedIdent.Type) + ")";
AddDeclaration(decl);
+ if (declHandler != null) declHandler.FuncDecl(f);
}
KnownFunctions.Add(f);
} else {
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);
}
|