I try to check satisfiability of x div y == 2 and x / y == 2 but got incorrect results both times. Looks like Z3 doesn't support these yet ?
(declare-fun x () Int)
(declare-fun y () Int)
(assert (= (div x y ) 2))
(check-sat)
(get-model)
(exit)
sat
(model
(define-fun y () Int
0)
(define-fun x () Int
38)
)
(declare-fun x () Int)
(declare-fun y () Int)
(assert (= (/ x y ) 2))
(check-sat)
(get-model)
(exit)
sat
(model
(define-fun y () Int
0)
(define-fun x () Int
1)
)
Integer division is supported, see: http://smtlib.cs.uiowa.edu/theories/Ints.smt2
Real division is also supported (from here: http://smtlib.cs.uiowa.edu/theories/Reals.smt2), the issue with division by zero you mention is covered:
"Since in SMT-LIB logic all function symbols are interpreted as total functions, terms of the form (/ t 0) are meaningful in every instance of Reals. However, the declaration imposes no constraints on their value. This means in particular that
- for every instance theory T and
- for every closed terms t1 and t2 of sort Real,
there is a model of T that satisfies (= t1 (/ t2 0))."
You should add an assertion that the divisor is not equal to zero.
(assert (not (= y 0)))
Here's the example (rise4fun link: http://rise4fun.com/Z3/IUDE ):
(declare-fun x () Int)
(declare-fun y () Int)
(assert (not (= y 0)))
(push)
(assert (= (div x y ) 2))
(check-sat)
(get-model) ; gives x = 2, y = 1
(pop)
(push)
(assert (= (/ x y ) 2))
(check-sat)
(get-model) ; gives x = -2, y = -1
(pop)
