From e686575ebf830e43ceae0c0310871739eb28ccc7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Thu, 28 May 2020 18:37:56 +0200 Subject: [PATCH] Only forbid private predicates in spec statements --- src/problem.rs | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/src/problem.rs b/src/problem.rs index 69597cb..353b1f2 100644 --- a/src/problem.rs +++ b/src/problem.rs @@ -86,10 +86,8 @@ impl Problem { match statement.kind { - crate::problem::StatementKind::CompletedDefinition(_) - | crate::problem::StatementKind::IntegrityConstraint - | crate::problem::StatementKind::Lemma(_) => continue, - _ => (), + crate::problem::StatementKind::Spec => (), + _ => continue, } if crate::formula_contains_predicate(&statement.formula, predicate_declaration)