--- a/NEWS Fri Apr 01 09:41:20 2022 +0200
+++ b/NEWS Fri Apr 01 09:58:05 2022 +0200
@@ -72,6 +72,12 @@
"sledgehammer_atp_problem_dest_dir", for problem files, and
"sledgehammer_atp_proof_dest_dir", for proof files. Minor INCOMPATIBILITY.
- Removed support for experimental prover 'z3_tptp'.
+ - The fastest successfully preplayed proof is always suggested.
+ - All SMT solvers but Z3 now resort to suggest (smt (verit)) when no proof
+ could be preplayed.
+ - Added new "some_preplayed" value to "expect" option to specify that some
+ successfully preplayed proof is expected. This is in contrast to the "some"
+ value which doesn't specify whether preplay succeeds or not.
* Mirabelle:
- Replaced sledgehammer option "keep" by
--- a/src/Doc/Sledgehammer/document/root.tex Fri Apr 01 09:41:20 2022 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex Fri Apr 01 09:58:05 2022 +0200
@@ -1157,6 +1157,7 @@
\begin{enum}
\item[\labelitemi] \textbf{\textit{some}:} Sledgehammer found a proof.
+\item[\labelitemi] \textbf{\textit{some\_preplayed}:} Sledgehammer found a proof that was successfully preplayed.
\item[\labelitemi] \textbf{\textit{none}:} Sledgehammer found no proof.
\item[\labelitemi] \textbf{\textit{timeout}:} Sledgehammer timed out.
\item[\labelitemi] \textbf{\textit{unknown}:} Sledgehammer encountered some