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.cs4
1 files changed, 2 insertions, 2 deletions
diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs
index d7c56d90..eaed83e9 100644
--- a/Source/Provers/SMTLib/TypeDeclCollector.cs
+++ b/Source/Provers/SMTLib/TypeDeclCollector.cs
@@ -268,7 +268,7 @@ void ObjectInvariant()
"(declare-fun " + printedName + " () " + TypeToString(node.Type) + ")";
if (!(printedName.StartsWith("assume$$") || printedName.StartsWith("soft$$") || printedName.StartsWith("try$$")))
{
- AddDeclaration(decl);
+ AddDeclaration(decl);
}
KnownVariables.Add(node);
if(declHandler != null)
@@ -311,7 +311,7 @@ void ObjectInvariant()
return;
}
- if (type.IsBool || type.IsInt || type.IsReal || type.IsFloat || type.IsBv)
+ if (type.IsBool || type.IsInt || type.IsReal || type.IsBv)
return;
CtorType ctorType = type as CtorType;