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/ProverInterface.cs   | 5 +++--
 Source/Provers/SMTLib/TypeDeclCollector.cs | 5 ++++-
 2 files changed, 7 insertions(+), 3 deletions(-)

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index b8fd2f50..7e98e8f8 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -411,10 +411,11 @@ namespace Microsoft.Boogie.SMTLib
       SendThisVC("(push 1)");
       SendThisVC("(set-info :boogie-vc-id " + SMTLibNamer.QuoteId(descriptiveName) + ")");
 
-      if (NamedAssumeVars != null)
+      if (CommandLineOptions.Clo.PrintNecessaryAssumes && NamedAssumeVars != null)
       {
         foreach (var v in NamedAssumeVars)
         {
+          SendThisVC(string.Format("(declare-fun {0} () Bool)", v));
           SendThisVC(string.Format("(assert (! {0} :named {1}))", v, "aux$$" + v.Name));
         }
       }
@@ -1292,7 +1293,7 @@ namespace Microsoft.Boogie.SMTLib
 
             var reporter = handler as VC.VCGen.ErrorReporter;
             // TODO(wuestholz): Is the reporter ever null?
-            if (NamedAssumeVars != null && NamedAssumeVars.Any() && result == Outcome.Valid && reporter != null)
+            if (CommandLineOptions.Clo.PrintNecessaryAssumes && NamedAssumeVars != null && NamedAssumeVars.Any() && result == Outcome.Valid && reporter != null)
             {
               SendThisVC("(get-unsat-core)");
               var resp = Process.GetProverResponse();
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