--- a/src/HOL/SMT.thy Sat Jun 17 17:41:02 2023 +0200
+++ b/src/HOL/SMT.thy Mon Jun 19 22:28:09 2023 +0200
@@ -660,9 +660,11 @@
ML_file \<open>Tools/SMT/z3_replay_methods.ML\<close>
ML_file \<open>Tools/SMT/z3_replay.ML\<close>
ML_file \<open>Tools/SMT/lethe_replay_methods.ML\<close>
+ML_file \<open>Tools/SMT/cvc5_replay_methods.ML\<close>
ML_file \<open>Tools/SMT/verit_replay_methods.ML\<close>
ML_file \<open>Tools/SMT/verit_strategies.ML\<close>
ML_file \<open>Tools/SMT/verit_replay.ML\<close>
+ML_file \<open>Tools/SMT/cvc5_replay.ML\<close>
ML_file \<open>Tools/SMT/smt_systems.ML\<close>
@@ -715,7 +717,7 @@
\<close>
declare [[cvc4_options = ""]]
-declare [[cvc5_options = ""]]
+declare [[cvc5_options = "--proof-format-mode=alethe --proof-granularity=dsl-rewrite"]]
declare [[verit_options = ""]]
declare [[z3_options = ""]]