Fix proof direction check

This commit is contained in:
Patrick Lühne 2020-05-28 06:30:14 +02:00
parent 870fdd048c
commit d72e2af49a
Signed by: patrick
GPG Key ID: 05F3611E97A70ABF

View File

@ -102,7 +102,7 @@ impl Problem
// If a backward proof is necessary, the program needs to be supertight, that is, no // If a backward proof is necessary, the program needs to be supertight, that is, no
// private predicates may transitively depend on themselves // 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() && predicate_declaration.is_self_referential()
{ {
return Err(crate::Error::new_private_predicate_cycle( return Err(crate::Error::new_private_predicate_cycle(