summaryrefslogtreecommitdiff
path: root/Source/Provers/SMTLib/TypeDeclCollector.cs
diff options
context:
space:
mode:
Diffstat (limited to 'Source/Provers/SMTLib/TypeDeclCollector.cs')
-rw-r--r--Source/Provers/SMTLib/TypeDeclCollector.cs5
1 files changed, 5 insertions, 0 deletions
diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs
index 05a6caf3..a4bdee51 100644
--- a/Source/Provers/SMTLib/TypeDeclCollector.cs
+++ b/Source/Provers/SMTLib/TypeDeclCollector.cs
@@ -164,6 +164,11 @@ void ObjectInvariant()
return TypeToString(t);
}
+ public void AddFunction(Function func) {
+ if (KnownFunctions.Contains(func))
+ return;
+ KnownFunctions.Add(func);
+ }
public override bool Visit(VCExprNAry node, bool arg) {
Contract.Requires(node != null);