Assume private predicates always

This commit is contained in:
Patrick Lühne 2020-05-28 06:30:35 +02:00
parent d72e2af49a
commit b80b3bf6d6
Signed by: patrick
GPG Key ID: 05F3611E97A70ABF
1 changed files with 3 additions and 0 deletions

View File

@ -225,6 +225,9 @@ impl Problem
statement.proof_status = ProofStatus::AssumedProven,
StatementKind::Lemma(ProofDirection::Forward) =>
statement.proof_status = ProofStatus::Ignored,
StatementKind::CompletedDefinition(ref predicate_declaration)
if !predicate_declaration.is_public() =>
statement.proof_status = ProofStatus::AssumedProven,
_ => statement.proof_status = ProofStatus::ToProveLater,
}
}