src/HOL/Tools/SMT/smt_solver.ML

           val out_path = Path.ext "smt_out" base_path
         in Cache_IO.raw_run mk_cmd input in_path out_path end
   | SOME certs =>
       (case Cache_IO.lookup certs input of
         (NONE, key) =>
-          if Config.get ctxt SMT_Config.fixed then
-            error ("Bad certificates cache: missing certificate")
+          if Config.get ctxt SMT_Config.read_only_certificates then
+            error ("Bad certificate cache: missing certificate")
           else
             Cache_IO.run_and_cache certs key mk_cmd input
       | (SOME output, _) =>
           trace_and ctxt ("Using cached certificate from " ^
             File.shell_path (Cache_IO.cache_path_of certs) ^ " ...")