Skip to content

v2.3.0

Compare
Choose a tag to compare
@hajduakos hajduakos released this 09 Sep 16:03
· 3144 commits to master since this release
9c0395d

This release introduces a breaking change in the syntax (and semantics) of bitvectors. Previously, bitvector variables could be declared with signedness information (signed/unsigned) and the operations relied on this information. With this release, bitvector variables no longer store their signedness (i.e., there is a single bitvector type with only the length as a parameter). Operations where signedness matters (e.g., comparison) come in two flavors (e.g., sgt for signed greater-than and ugt for unsigned greater-than). This aligns with the way SMT-LIB and LLVM works. Thanks @as3810t! See bitvectors.md for more information.