# HG changeset patch
# User wenzelm
# Date 1738840736 -3600
# Node ID 2c9c06a9f61fbd09f547b82ba706531d0748f349
# Parent  023845c29d48fb69198bc13a783ddf7ca4e28f12
tuned;

diff -r 023845c29d48 -r 2c9c06a9f61f src/HOL/Tools/SMT/smt_solver.ML
--- a/src/HOL/Tools/SMT/smt_solver.ML	Thu Feb 06 12:07:47 2025 +0100
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Thu Feb 06 12:18:56 2025 +0100
@@ -137,12 +137,12 @@
 
 in
 
-fun invoke memoize_fun_call name command options smt_options ithms ctxt =
+fun invoke memoize_fun_call name command cmd_options smt_options ithms ctxt =
   let
-    val options = options @ SMT_Config.solver_options_of ctxt
+    val options = cmd_options @ SMT_Config.solver_options_of ctxt
     val comments = [implode_space options]
 
-    val (str, replay_data as {context = ctxt', ...}) =
+    val (input, replay_data as {context = ctxt', ...}) =
       ithms
       |> tap (trace_assms ctxt)
       |> SMT_Translate.translate ctxt name smt_options comments
@@ -153,8 +153,8 @@
 
     val output_lines =
       (case memoize_fun_call of
-        NONE => run_cmd str
-      | SOME memoize => split_lines (memoize (cat_lines o run_cmd) str))
+        NONE => run_cmd input
+      | SOME memoize => split_lines (memoize (cat_lines o run_cmd) input))
   in (output_lines, replay_data) end
 
 end