Give values to BV constants when cloning
The BV constants one
, ones
, zero
and zeros
should be given values when cloning, e.g. BV32 etc., instead of being given in SMT2 driver.
The impact on proofs and on CEs and CE checking should be carefully checked.