CODEWITHSUNDEEP
z3smt
arrowd
arrowd

Reputation: 34401

How to zero/sign extend bitvectors in Z3?

I was unable to perform zero extension on a bitvector using Z3 SMT interface. From what I've learned by reading sources, there are functions for this, and they are available for various bindings (C, C++, Python, etc.), but the tutorial for SMT interface gives no clue how to call them.

Using zero_extend from the SMT QF_BV logic standard doesn't help too - Z3 says unsupported.

Upvotes: 3

Views: 1452

Answers (1)

arrowd
arrowd

Reputation: 34401

It turned out that zero_extend and some other functions are parametric ones, probably something like foo<T> in C++. To call such functions one need to use special syntax:

(declare-const a (_ BitVec 1))
(declare-const b (_ BitVec 2))
(assert (= b ((_ zero_extend 1) a)))
(check-sat)
(get-model)

Using ((_ zero_extend i) x) instead of (zero_extend i x) gives correct result:

sat
(model
  (define-fun a () (_ BitVec 1) #b0)
  (define-fun b () (_ BitVec 2) #b00)
)

Upvotes: 4

Related Questions