diff options
| author |  Valentin Wüstholz <wuestholz@gmail.com> | 2015-12-28 20:28:04 -0600 |
|---|---|---|
| committer | Valentin Wüstholz <wuestholz@gmail.com> | 2015-12-28 20:28:04 -0600 |
| commit | 5d23ab3bf5bc80ee1bf5bbc6194a6de67264c61f (patch) | |
| tree | 95117d025f135f5fb0bad394a8864409cb50f535 /Source/Provers/SMTLib/TypeDeclCollector.cs | |
| parent | dd8e69b7b71a9375b7206a70633deae234175ef8 (diff) | |
Fix issue with ids for assume-statements.
Diffstat (limited to 'Source/Provers/SMTLib/TypeDeclCollector.cs')
| -rw-r--r-- | Source/Provers/SMTLib/TypeDeclCollector.cs | 5 |
1 files changed, 4 insertions, 1 deletions
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); |