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, 4 insertions, 1 deletions
diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs
index 32e28560..1c23c22f 100644
--- a/Source/Provers/SMTLib/TypeDeclCollector.cs
+++ b/Source/Provers/SMTLib/TypeDeclCollector.cs
@@ -255,7 +255,10 @@ void ObjectInvariant()
RegisterType(node.Type);
string decl =
"(declare-fun " + printedName + " () " + TypeToString(node.Type) + ")";
- AddDeclaration(decl);
+ if (!printedName.StartsWith("assume$$"))
+ {
+ AddDeclaration(decl);
+ }
KnownVariables.Add(node);
if(declHandler != null)
declHandler.VarDecl(node);