From e97989c069ef1f30152095c667c45338edb28434 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Wed, 15 May 2024 10:09:09 -0400 Subject: [PATCH] CHANGES.md: Mention #258 --- what4/CHANGES.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/what4/CHANGES.md b/what4/CHANGES.md index be523ad3..2df6bf71 100644 --- a/what4/CHANGES.md +++ b/what4/CHANGES.md @@ -14,6 +14,9 @@ * Add support for the `bitwuzla` SMT solver. +* Add `bvZero` and `bvOne` functions, which are convenient shorthand for + constructing bitvectors with the values `0` and `1`, respectively. + * Add `pushMuxOps` and `pushMuxOpsOption`. If this option is enabled, What4 will push certain `ExprBuilder` operations (e.g., `zext`) down to the branches of `ite` expressions. In some (but not all) circumstances, this can result in