summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Source/Provers/SMTLib/ProverInterface.cs5
-rw-r--r--Source/Provers/SMTLib/TypeDeclCollector.cs5
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);