CODEWITHSUNDEEP
z3
Zvonimir
Zvonimir

Reputation: 21

Z3 returning unknown for a simple query involving integer division

Here is a simple Z3 query that involves integer division (i.e., nonlinear operations):

(declare-const a01 Int)
(declare-const a02 Int)
(assert(or (= (/ a01 a02) 2) (= (/ a02 a01) 2)))
(assert( > a01 0))
(assert( > a02 0))
(check-sat)

Z3 returns uknown for when attempting to solve this query. I understand that nonlinear integer arithmetic is undecidable, but I was still hoping that Z3 would be a bit less fragile in practice.

Please let me know if I am missing some obvious parameters that I could set for Z3 to help it to solve such queries. I am using Z3 4.4.1 and I tried the version on rise4fun too. Thanks!

Upvotes: 2

Views: 72

Answers (1)

mmpourhashem
mmpourhashem

Reputation: 91

Use div instead of /.

(declare-const a01 Int)
(declare-const a02 Int)
(assert(or (= (div a01 a02) 2) (= (div a02 a01) 2)))
(assert( > a01 0))
(assert( > a02 0))
(check-sat)

Upvotes: 0

Related Questions