New SMT2 backend: arithmetic operators implementation for fixed size bit vectors#6614

Merged

NlightNFotis merged 9 commits intodiffblue:developfrom

NlightNFotis:newsmt_additional_operators

Feb 3, 2022

Commits on Feb 3, 2022

Add implementation of arithmetic operator `bvadd`.
NlightNFotis
committed
Add implementation of arithmetic operator `bvsub`.
NlightNFotis
committed
Add implementation of multiplication operator `bvmul`.
NlightNFotis
committed
Add implementation of (unsigned) division operator `bvudiv`.
NlightNFotis
committed
Add implementation of (signed) division operator (`bvsdiv`).
NlightNFotis
committed
Add (unsigned) remainder (modulus) arithmetic operator `bvurem`.
NlightNFotis
committed
Add implementation of signed remainder operator (`bvsrem`).
NlightNFotis
committed
Add implementation of negation (unary minus - `bvneg`) operator.
NlightNFotis
committed
Rename `validate_bit_vector_predicate_arguments` to `validate_bit_vector_operator_arguments`.
NlightNFotis
committed