# HG changeset patch # User desharna # Date 1632820304 -7200 # Node ID d5e034f2c109f4479b98dda18005456b166f80f2 # Parent d8dc8fdc46fc913da9fbd257ca21c4bb189431db fixed veriT environment variable in sledgehammer's documentation diff -r d8dc8fdc46fc -r d5e034f2c109 src/Doc/Sledgehammer/document/root.tex --- a/src/Doc/Sledgehammer/document/root.tex Tue Sep 28 10:47:18 2021 +0200 +++ b/src/Doc/Sledgehammer/document/root.tex Tue Sep 28 11:11:44 2021 +0200 @@ -192,7 +192,7 @@ number (e.g., ``3.6''). Similarly, if you want to install CVC4, veriT, or Z3, set the environment -variable \texttt{CVC4\_\allowbreak SOLVER}, \texttt{VERIT\_\allowbreak SOLVER}, +variable \texttt{CVC4\_\allowbreak SOLVER}, \texttt{ISABELLE\_\allowbreak VERIT}, or \texttt{Z3\_SOLVER} to the complete path of the executable, \emph{including the file name}. Ideally, also set \texttt{CVC4\_VERSION}, \texttt{VERIT\_VERSION}, or \texttt{Z3\_VERSION} to the solver's version number @@ -742,7 +742,7 @@ \item[\labelitemi] \textbf{\textit{verit}:} veriT \cite{bouton-et-al-2009} is an SMT solver developed by David D\'eharbe, Pascal Fontaine, and their colleagues. It is designed to produce detailed proofs for reconstruction in proof -assistants. To use veriT, set the environment variable \texttt{VERIT\_SOLVER} +assistants. To use veriT, set the environment variable \texttt{ISABELLE\_VERIT} to the complete path of the executable, including the file name. \item[\labelitemi] \textbf{\textit{z3}:} Z3 is an SMT solver developed at