GaloisInc/what4
1
1
Fork 0
mirror of https://github.com/GaloisInc/what4.git synced 2024-08-16 07:30:29 +03:00
Code Issues Projects Releases Wiki Activity

CHANGES.md: Mention #258

Browse Source
This commit is contained in:
Ryan Scott 2024-05-15 10:09:09 -04:00
parent 97643c4a86
commit e97989c069
1 changed files with 3 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
what4/CHANGES.md
View File

@ -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