splitted option "smt_debug_files" into "smt_problem_dest_dir" and "smt_proof_dest_dir"

--- a/NEWS	Wed Oct 01 11:17:35 2025 +0000
+++ b/NEWS	Wed Oct 01 11:18:23 2025 +0000
@@ -201,6 +201,8 @@
     support for datatypes and vampire_smt_nodt does not).
   - Added SMT solver "dummy_smtlib" which immediately fails; this is useful
     when generating SMT-LIB files with Mirabelle.
+  - Splitted option "smt_debug_files" into "smt_problem_dest_dir" and
+    "smt_proof_dest_dir". Minor INCOMPATIBILITY.
 
 * Theory "HOL.Fun":
   - Added lemmas.

--- a/src/HOL/TPTP/mash_eval.ML	Wed Oct 01 11:17:35 2025 +0000
+++ b/src/HOL/TPTP/mash_eval.ML	Wed Oct 01 11:18:23 2025 +0000
@@ -108,7 +108,8 @@
               in
                 Config.put atp_problem_dest_dir dir
                 #> Config.put atp_problem_prefix (prob_prefix ^ "__")
-                #> Config.put SMT_Config.debug_files (dir ^ "/" ^ prob_prefix)
+                #> Config.put SMT_Config.problem_dest_file (dir ^ "/" ^ prob_prefix)
+                #> Config.put SMT_Config.proof_dest_file (dir ^ "/" ^ prob_prefix)
               end
             | set_file_name _ NONE = I
 

--- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML	Wed Oct 01 11:17:35 2025 +0000
+++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML	Wed Oct 01 11:18:23 2025 +0000
@@ -139,7 +139,11 @@
             Config.put Sledgehammer_Prover_ATP.atp_problem_prefix (filename ^ "__")
             #> (keep_probs ? Config.put Sledgehammer_Prover_ATP.atp_problem_dest_dir dir)
             #> (keep_proofs ? Config.put Sledgehammer_Prover_ATP.atp_proof_dest_dir dir)
-            #> Config.put SMT_Config.debug_files (dir ^ "/" ^ filename ^ "__" ^ serial_string ())
+            #> (keep_probs ? Config.put SMT_Config.problem_dest_file
+                  (dir ^ "/" ^ filename ^ "__" ^ serial_string ()))
+            #> (keep_proofs ? Config.put Sledgehammer_Prover_ATP.atp_proof_dest_dir dir)
+            #> Config.put SMT_Config.proof_dest_file
+                  (dir ^ "/" ^ filename ^ "__" ^ serial_string ())
           end
         | set_file_name NONE = I
       val state' = state

--- a/src/HOL/Tools/SMT/smt_config.ML	Wed Oct 01 11:17:35 2025 +0000
+++ b/src/HOL/Tools/SMT/smt_config.ML	Wed Oct 01 11:18:23 2025 +0000
@@ -38,7 +38,8 @@
   val native_bv: bool Config.T
   val nat_as_int: bool Config.T
   val infer_triggers: bool Config.T
-  val debug_files: string Config.T
+  val problem_dest_file : string Config.T
+  val proof_dest_file : string Config.T
   val sat_solver: string Config.T
   val compress_verit_proofs: Proof.context -> bool
 
@@ -191,7 +192,8 @@
 val native_bv = Attrib.setup_config_bool \<^binding>\<open>native_bv\<close> (K true);
 val nat_as_int = Attrib.setup_config_bool \<^binding>\<open>smt_nat_as_int\<close> (K false);
 val infer_triggers = Attrib.setup_config_bool \<^binding>\<open>smt_infer_triggers\<close> (K false);
-val debug_files = Attrib.setup_config_string \<^binding>\<open>smt_debug_files\<close> (K "");
+val problem_dest_file = Attrib.setup_config_string \<^binding>\<open>smt_problem_dest_dir\<close> (K "");
+val proof_dest_file = Attrib.setup_config_string \<^binding>\<open>smt_proof_dest_dir\<close> (K "");
 val sat_solver = Attrib.setup_config_string \<^binding>\<open>smt_sat_solver\<close> (K "cdclite");
 val cvc_experimental_lethe = Attrib.setup_config_bool \<^binding>\<open>smt_cvc_lethe\<close> (K false);
 

--- a/src/HOL/Tools/SMT/smt_solver.ML	Wed Oct 01 11:17:35 2025 +0000
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Wed Oct 01 11:18:23 2025 +0000
@@ -69,16 +69,27 @@
     NONE =>
       if not (SMT_Config.is_available ctxt name) then
         error ("The SMT solver " ^ quote name ^ " is not installed")
-      else if Config.get ctxt SMT_Config.debug_files = "" then
-        with_trace ctxt ("Invoking SMT solver " ^ quote name ^ " ...") (Cache_IO.run cmd) input
       else
         let
-          val base_path = Path.explode (Config.get ctxt SMT_Config.debug_files)
-          val in_path = Path.ext "smt_in" base_path
-          val out_path = Path.ext "smt_out" base_path
-          val _ = File.write in_path input
-          val result = Cache_IO.run cmd input
-          val _ = Bytes.write out_path (Bytes.terminate_lines (Process_Result.out_lines result))
+          val () =
+            (case Config.get ctxt SMT_Config.problem_dest_file of
+              "" => ()
+            | base_path =>
+              let val in_path = Path.ext "smt_in" (Path.explode base_path) in
+                File.write in_path input
+              end)
+          val result =
+            with_trace ctxt ("Invoking SMT solver " ^ quote name ^ " ...") (Cache_IO.run cmd) input
+          val () =
+            (case Config.get ctxt SMT_Config.proof_dest_file of
+              "" => ()
+            | base_path =>
+              let
+                val out_path = Path.ext "smt_out" (Path.explode base_path)
+                val output = Bytes.terminate_lines (Process_Result.out_lines result)
+              in
+                Bytes.write out_path output
+              end)
         in result end
   | SOME certs =>
       (case Cache_IO.lookup certs input of

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Wed Oct 01 11:17:35 2025 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Wed Oct 01 11:18:23 2025 +0000
@@ -86,8 +86,13 @@
            SOME nat_as_int => Config.put SMT_Config.nat_as_int nat_as_int
          | NONE => I)
       |> (if overlord then
-            Config.put SMT_Config.debug_files
-              (overlord_file_location_of_prover name |> (fn (path, name) => path ^ "/" ^ name))
+            let
+              val (path, name) = overlord_file_location_of_prover name
+              val file_base = path ^ "/" ^ name
+            in
+              Config.put SMT_Config.problem_dest_file file_base #>
+              Config.put SMT_Config.proof_dest_file file_base
+            end
           else
             I)
        |> Config.put SMT_Config.infer_triggers (Config.get ctxt smt_triggers)