Skip to content
Snippets Groups Projects
Commit f8dcee14 authored by Hans-Jörg's avatar Hans-Jörg
Browse files

Add list of rules that are only used by cvc5

parent 23afe318
No related branches found
No related tags found
No related merge requests found
Pipeline #24175 passed
......@@ -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}
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment