diff options
author | Valentin Wüstholz <wuestholz@gmail.com> | 2016-03-09 19:18:15 -0600 |
---|---|---|
committer | Valentin Wüstholz <wuestholz@gmail.com> | 2016-03-09 19:37:25 -0600 |
commit | 8ed5dab22d8377924ee6282b83c1b1f8aa8f3573 (patch) | |
tree | 8065119c09552703a6ea9634eb22f6b5a6951734 /Source/Provers/SMTLib/TypeDeclCollector.cs | |
parent | 63c4b7642cd4566a39906b2d73c47b4ebe9f7c1c (diff) |
Improve support for identifying unnecessary assumes.
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); } |