Is this a bug for division in Z3?

Question

I tried in rise4fun with the following two scripts:

Script(1):

(declare-const a Int)
(declare-const b Int)
(assert (= 1 (/ a b))) ; division
(check-sat)
(get-model)

Script(2):

(declare-const a Int)
(declare-const b Int)
(assert (= 1 (rem a b))) ; remainder
(check-sat)
(get-model)

Z3 gave me (a=0, b=0) as the model of script(1) and (a=38, b=0) as the model of script(2), which are obviously wrong. Do these solutions indicate some bugs in Z3? Thanks!

Answer 1

This is not a bug, but due to how functions are defined mathematically in SMT and Z3. The problem is that you do not have any assertion that the denominator is not zero, so you have a division by zero in both of these cases. If you add the constraint that b is not zero, this will give you the more expected result. Here are your updated examples that give the more expected results (rise4fun link: http://rise4fun.com/Z3/Xokpp ):

(declare-const a Int)
(declare-const b Int)
(assert (= 1 (/ a b))) ; 
(check-sat)
(get-model) ; gives a = 0, b = 0

(assert (not (= b 0)))
(check-sat)
(get-model) ; gives a = -1, b = -1

And (rise4fun link: http://rise4fun.com/Z3/x5Is ):

(declare-const a Int)
(declare-const b Int)
(assert (= 1 (rem a b)))
(check-sat)
(get-model) ; gives b = 0, a = 38

(assert (not (= b 0)))
(check-sat)
(get-model) ; gives b = 2, a = 1

For more details, see also this question and answer (it talks more about reals, but the situation is similar for integers, and the integer theory refers to how division is handled in the real theory):

integer division gives incorrect result