diff options
Diffstat (limited to 'Source/Provers/SMTLib/TypeDeclCollector.cs')
| -rw-r--r-- | Source/Provers/SMTLib/TypeDeclCollector.cs | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs index d911ce58..eaed83e9 100644 --- a/Source/Provers/SMTLib/TypeDeclCollector.cs +++ b/Source/Provers/SMTLib/TypeDeclCollector.cs @@ -217,7 +217,10 @@ void ObjectInvariant() } else if (node.Op.Equals(VCExpressionGenerator.NamedAssumeOp)) { var exprVar = node[0] as VCExprVar; AddDeclaration(string.Format("(declare-fun {0} () Bool)", exprVar.Name)); - AddDeclaration(string.Format("(assert (! {0} :named {1}))", exprVar.Name, "aux$$" + exprVar.Name)); + if (CommandLineOptions.Clo.PrintNecessaryAssumes) + { + AddDeclaration(string.Format("(assert (! {0} :named {1}))", exprVar.Name, "aux$$" + exprVar.Name)); + } } else { VCExprBoogieFunctionOp op = node.Op as VCExprBoogieFunctionOp; if (op != null && @@ -263,7 +266,7 @@ void ObjectInvariant() RegisterType(node.Type); string decl = "(declare-fun " + printedName + " () " + TypeToString(node.Type) + ")"; - if (!(printedName.StartsWith("assume$$") || printedName.StartsWith("soft$$"))) + if (!(printedName.StartsWith("assume$$") || printedName.StartsWith("soft$$") || printedName.StartsWith("try$$"))) { AddDeclaration(decl); } |