search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.29k stars 1.48k forks source link

How to make size of BitVec compatible #2900

Closed tintinlam007 closed 4 years ago

tintinlam007 commented 4 years ago

(declare-const A ( BitVec 8)) (declare-const B ( BitVec 4)) (assert (= A #x01)) (assert (= A B)) (check-sat) (get-model)

z3 has got error because size of BitVec incompatible. How to transformat BitVec size? thank you~

wintersteiger commented 4 years ago

Use the zero_extend or sign_extend operator as defined in smt-lib here: http://smtlib.cs.uiowa.edu/Logics/QF_BV.smt2