From c1038b398ceecb480613e95824ac0d9ba74b854d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Tue, 19 May 2020 12:47:24 +0200 Subject: [PATCH] Improve warning when using private predicates in specification --- src/error.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/error.rs b/src/error.rs index 12ae716..0fc3f56 100644 --- 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) =>