--- a/src/Doc/Sledgehammer/document/root.tex Wed Oct 23 16:09:24 2019 +0000
+++ b/src/Doc/Sledgehammer/document/root.tex Fri Oct 25 13:25:30 2019 +0200
@@ -190,11 +190,12 @@
for Alt-Ergo, set the environment variable \texttt{WHY3\_HOME} to the
directory that contains the \texttt{why3} executable. Sledgehammer has been
tested with AgsyHOL 1.0, Alt-Ergo 0.95.2, E 1.6 to 2.0, LEO-II 1.3.4, Leo-III
-1.1, and Satallax 2.2 to 2.7. Since the ATPs' output formats are neither
-documented nor stable, other versions might not work well with Sledgehammer.
-Ideally, you should also set \texttt{E\_VERSION}, \texttt{LEO2\_VERSION},
+1.1, and Satallax 2.7. Since the ATPs' output formats are neither documented
+nor stable, other versions might not work well with Sledgehammer. Ideally, you
+should also set \texttt{E\_VERSION}, \texttt{LEO2\_VERSION},
\texttt{LEO3\_VERSION}, or \texttt{SATALLAX\_VERSION} to the prover's version
-number (e.g., ``2.7'').
+number (e.g., ``2.7''); this might help Sledgehammer invoke the prover
+optimally.
Similarly, if you want to install CVC3, CVC4, veriT, or Z3, set the environment
variable \texttt{CVC3\_\allowbreak SOLVER}, \texttt{CVC4\_\allowbreak SOLVER},
--- a/src/HOL/Tools/ATP/atp_systems.ML Wed Oct 23 16:09:24 2019 +0000
+++ b/src/HOL/Tools/ATP/atp_systems.ML Fri Oct 25 13:25:30 2019 +0200
@@ -472,6 +472,9 @@
val satallax_config : atp_config =
{exec = K (["SATALLAX_HOME"], ["satallax.opt", "satallax"]),
arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
+ (case getenv "E_HOME" of
+ "" => ""
+ | home => "-E " ^ home ^ "/eprover ") ^
"-p tstp -t " ^ string_of_int (to_secs 1 timeout) ^ " " ^ file_name,
proof_delims =
[("% SZS output start Proof", "% SZS output end Proof")],