From 826f644f1203a9abf8d07e9f4a4bf5c78e76626f Mon Sep 17 00:00:00 2001 From: Hans-Joerg Schurr <commits@schurr.at> Date: Mon, 18 Mar 2024 19:47:48 -0500 Subject: [PATCH] Update changelog: bitvector rules --- spec/changelog.tex | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/spec/changelog.tex b/spec/changelog.tex index 4f0b57a..aeec219 100644 --- a/spec/changelog.tex +++ b/spec/changelog.tex @@ -1,5 +1,13 @@ \subsection*{Unreleased} +Proof rules: +\begin{itemize} + \item Addition of a section describing bitvector proofs. + \item Bitblasting rules: \proofRule{bitblast_extract}, \proofRule{bitblast_add}, + \proofRule{bitblast_ult}. +\end{itemize} + +\noindent Breaking changes: \begin{itemize} \item Allow arbitrary extra annotations in \texttt{assume} commands. -- GitLab