CODEWITHSUNDEEP
z3
Student Popper
Student Popper

Reputation: 103

How do I describe integer division in programming language this in Z3?

I am using SMT solver to help to analyze programs. In programming languages, the following condition is satisfiable:

int x;
if((x/2) * 2 != x)  {
//reachable
}

but for the integer type in mathmatics, this is not satisfiable. Can I use Z3 to describe this? Thanks.

Upvotes: 1

Views: 950

Answers (1)

pad
pad

Reputation: 41290

Your example is also satisfiable in mathematical integer. You can find a model for x to be any odd integer.

In Z3, you should use machine integer i.e. bit-vectors for modeling:

(declare-const x (_ BitVec 32))
(assert (not (= (bvmul (bvsdiv x (_ bv2 32)) (_ bv2 32)) x)))
(check-sat)
(get-model)

This examplerise4fun link is indeed satisfiable.

Upvotes: 1

Related Questions