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)))))))

Answer 2

As far as I can tell, your assertion that the last equation is inconsistent does not match the documentation of the SMT-LIB standard. The page Theories: Reals says:

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 value v (as defined in the :values attribute) and closed term t of sort Real,

there is a model of T that satisfies (= v (/ t 0)).

Similarly, the page Theories: Ints says:

See note in the Reals theory declaration about terms of the form (/ t 0).

The same observation applies here to terms of the form (div t 0) and (mod t 0).

Therefore, it stands to reason to believe that no SMT-LIB compliant tool would ever print unsat for the given formula.