# HG changeset patch # User wenzelm # Date 1615754488 -3600 # Node ID 5614aab3f83e9ac0104f95d7d102c644390bbf82 # Parent e92f2e44e4d8dcaf887c2769aa25f6f161a685da proper shell quote; diff -r e92f2e44e4d8 -r 5614aab3f83e src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML --- 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,