diff --git a/spec/rule_list.tex b/spec/rule_list.tex
index 66d20af4cc04be62541992486598f5fb512acda0..663a4efe1a446d18cd9eeea10455a2f19fe0437f 100644
--- a/spec/rule_list.tex
+++ b/spec/rule_list.tex
@@ -243,6 +243,17 @@ simplifications.}
 \ruleref{bitblast_add} & Bitblasting of $\lsymb{add}$. \\
 \end{xltabular}
 
+\begin{xltabular}{\linewidth}{l X}
+\caption{Rules used by cvc5, but not by veriT.}
+\label{rule-tab:cvc5}\\
+  Rule & Description \\
+  \hline
+\ruleref{bitblast_extract} & Bitblasting of $\lsymb{extract}$. \\
+\ruleref{bitblast_ult} & Bitblasting of $\lsymb{ult}$. \\
+\ruleref{bitblast_add} & Bitblasting of $\lsymb{add}$. \\
+\ruleref{la_mult_pos} & Multiplication with a positive factor. \\
+\ruleref{la_mult_neg} & Multiplication with a negative factor.\\
+\end{xltabular}
 \subsection{Rule List}
 \label{sec:alethe:rules-list}