Skip to content

v0.1.1

Latest
Latest
Compare
Choose a tag to compare
@elsoroka elsoroka released this 17 Dec 00:43
· 24 commits to main since this release
Releases
0322f6f
This commit was created on GitHub.com and signed with GitHub’s verified signature. The key has expired.
GPG key ID: 4AEE18F83AFDEB23
Expired
Learn about vigilant mode.
  • Fixed bugs in issues #21 and #26.
    *Added remaining operators defined in SMT-LIB QF_BV (bitvector) specification (issue #22)
  • Add ^ for square
  • Correctly promote expressions containing mixed BoolExpr, IntExpr and RealExpr types. When a Boolean variable z is used in an arithmetic expression, it is rewritten to ite(z 1 0) (int) or ite(z 1.0 0.0) (real), which matches Z3's behavior. The SMT-LIB functions to_real and to_int are used to convert mixed IntExprs and RealExprs.
Assets 2