From d72e2af49a8cd8682c21f9c96682168aeb2cf105 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Thu, 28 May 2020 06:30:14 +0200 Subject: [PATCH] Fix proof direction check --- src/problem.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/problem.rs b/src/problem.rs index e1f550c..a0433f4 100644 --- a/src/problem.rs +++ b/src/problem.rs @@ -102,7 +102,7 @@ impl Problem // If a backward proof is necessary, the program needs to be supertight, that is, no // private predicates may transitively depend on themselves - if proof_direction.requires_forward_proof() && !predicate_declaration.is_public() + if proof_direction.requires_backward_proof() && !predicate_declaration.is_public() && predicate_declaration.is_self_referential() { return Err(crate::Error::new_private_predicate_cycle(