Closed mmcloughlin closed 11 months ago
Currently the solver outputs for example bv-1 for negative constant values, which is invalid SMT and causes an error.
bv-1
This PR updates the bv method in the solver to produce bvneg of the positive constant in this case.
bv
bvneg
Currently the solver outputs for example
bv-1
for negative constant values, which is invalid SMT and causes an error.This PR updates the
bv
method in the solver to producebvneg
of the positive constant in this case.