Is it possible to detect inconsistent equations in Z3, or before passing to Z3?

Question

I was working with z3 with the following example.

f=Function('f',IntSort(),IntSort())
n=Int('n')
c=Int('c')
s=Solver()
s.add(c>=0)
s.add(f(0)==0)
s.add(ForAll([n],Implies(n>=0, f(n+1)==f(n)+10/(n-c))))

The last equation is inconsistent (since n=c would make it indeterminate). But, Z3 cannot detect this kind of inconsistencies. Is there any way in which Z3 can be made to detect it, or any other tool that can detect it?

Answer 1

Z3 does not check for division by zero because, as Patrick Trentin mentioned, the semantics of division by zero according to SMT-LIB are that it returns an unknown value.

You can manually ask Z3 to check for division by zero, to ensure that you never depend division by zero. (This is important, for example, if you are modeling a language where division by zero has a different semantics from SMT-LIB.)

For your example, this would look as follows:

(declare-fun f (Int) Int)

(declare-const c Int)

(assert (>= c 0))

(assert (= (f 0) 0))

; check for division by zero
(push)
(declare-const n Int)
(assert (>= n 0))

(assert (= (- n c) 0))
(check-sat)  ; reports sat, meaning division by zero is possible
(get-model)  ; an example model where division by zero would occur
(pop)

;; Supposing the check had passed (returned unsat) instead, we could
;; continue, safely knowing that division by zero could not happen in
;; the following.
(assert (forall ((n Int)) 
                (=> (>= n 0) 
                    (= (f (+ n 1)) 
                       (+ (f n) (/ 10 (- n c)))))))