The bit-width transformation of bit vectors

Skip to first unread message


Aug 28, 2017, 7:05:35 AM8/28/17
to pySMT
Hello Everyone!

I am using bitvector to implement efficient computing.
As we all know that adding two 8-bit numbers, we need a 9-bit width; 
whereas multiplying two 8-bit numbers, we need a 16-bit width.

Is there any methods to switch the bit-width of each bitvectors?

Because I have tried:

A = BV(240,9)
B = BV(200,9)
Upper_bound = BV(255,8)
C = BVAdd(A,B)
C = BV(C,8)
C = max(C,Upper_bound) # To ensure the upper bound is 255 in 8-bit

Then it shows:
pysmt.exceptions.PysmtTypeError: Invalid type in constant. The type was:<class 'pysmt.fnode.FNode'>
which refers that C = BV(C,8) is illegal

Andrea Micheli

Aug 31, 2017, 4:47:16 AM8/31/17
to 陳宏毅, pySMT

in SMT the width of each BV variable must be fixed, there is no way to dynamically extend it to avoid overflows. Moreover the arithmetic operations (such as BVAdd) take in input two bit-vectors of size w and return a bit vector of size w. Of course, there is the possibility of overflow or underflow in the operations, but those are well-defined in the logic and expected. You can think of BV as a logic that allows to express formulae over the computation of microprocessors or hardware in general.

If you want to represent numeric operations without overflows or underflows and you can limit your encoding to a linear formula, you should try to use the Linear Integer Arithmetic (LIA) logic instead of BV.

Otherwise you need to over-approximate the bit-width necessary for your problem and the use this bit width for all your variables.



You received this message because you are subscribed to the Google Groups "pySMT" group.
To unsubscribe from this group and stop receiving emails from it, send an email to
To post to this group, send email to
To view this discussion on the web visit
For more options, visit

Reply all
Reply to author
0 new messages