Improve warning when using private predicates in specification

2020-05-19 12:47:24 +02:00 · 2020-05-19 12:47:24 +02:00 · c1038b398c
parent 3bf981236a
commit c1038b398c
1 changed files with 1 additions and 1 deletions
--- a/src/error.rs
+++ b/src/error.rs
@ -251,7 +251,7 @@ impl std::fmt::Debug for Error
 					predicate_declaration),
 			Kind::PredicateShouldNotOccurInSpecification(ref predicate_declaration) =>
 				write!(formatter,
-					"predicate {} should not occur in specification (it is not declared as an input or output predicate)",
+					"{} should not occur in specification because it’s a private predicate (consider declaring it an input or output predicate)",
 					predicate_declaration),
 			Kind::RunVampire => write!(formatter, "could not run Vampire"),
 			Kind::ProveProgram(exit_code, ref stdout, ref stderr) =>