Mention overlappable addition to queriables

LeventErkok · Aug 10, 2024 · abc1561 · abc1561
1 parent c486c20
commit abc1561
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 1 deletion.
diff --git a/CHANGES.md b/CHANGES.md
@@ -5,6 +5,9 @@
 
   * Fix a few custom-floating-point format conversion bugs. Thanks to Sirui Lu for the patch.
 
+  * Add a few OVERLAPPABLE pragms to generic Queriable instances to make them easily overridable by
+    user programs. Thanks to Marco Zocca for reporting.
+
   * Add signedMulOverflow, which checks whether multiplication of two signed-bitvectors can overflow.
     SBV already had a method (bvMulO) that served this purpose, translating to the corresponding predicate
     in SMTLib. Unfortunately not all solvers support this predicate efficiently. In particular, as of Aug 2024,

diff --git a/README.md b/README.md
@@ -176,6 +176,7 @@ May Torrence,
 Daniel Wagner,
 Sean Weaver,
 Nis Wegmann,
-and Jared Ziegler.
+Jared Ziegler,
+and Marco Zocca.
 
 Thanks!