From 5d23ab3bf5bc80ee1bf5bbc6194a6de67264c61f Mon Sep 17 00:00:00 2001
From: Valentin Wüstholz <wuestholz@gmail.com>
Date: Mon, 28 Dec 2015 20:28:04 -0600
Subject: Fix issue with ids for assume-statements.

---
 Source/Provers/SMTLib/TypeDeclCollector.cs | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'Source/Provers/SMTLib/TypeDeclCollector.cs')

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);
-- 
cgit v1.2.3