--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Sun Mar 14 21:02:34 2021 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Sun Mar 14 21:41:28 2021 +0100
@@ -366,7 +366,7 @@
val leo3_config : atp_config =
{exec = (["LEO3_HOME"], ["leo3"]),
arguments = fn _ => fn full_proofs => fn _ => fn timeout => fn problem => fn _ =>
- File.bash_path problem ^ " " ^ "--atp cvc=$CVC4_SOLVER --atp e=\"$E_HOME\"/eprover \
+ File.bash_path problem ^ " " ^ "--atp cvc=\"$CVC4_SOLVER\" --atp e=\"$E_HOME\"/eprover \
\-p -t " ^ string_of_int (to_secs 1 timeout) ^ " " ^
(if full_proofs then "--nleq --naeq " else ""),
proof_delims = tstp_proof_delims,