Z3 does not solve quantifier expression, expression is sat

Question

Using z3 v 4.8.1 - - 64 bit - build hashcode 016872a5e0f6 the script below evaluate to unsat but an result of sat is expected.

• Does z3 support solving expression like these?

• Can a different smt-solver solve expression like these?

  (set-option :print-success false)
  (set-logic ALL)
  (push 1)
  (declare-const ss1 Int)
  (declare-const ss3 Int)
  
  (assert (forall ((t_ss3 Int)(t_ss1 Int))
  (=>
    (< t_ss1 t_ss3)
    (and (and
     (< ss1 ss3)
     (= t_ss1 ss1))
     (= t_ss3 ss3))
  )))
  (echo "Check if the P -> Q is satisfiable")
  (check-sat)
  (pop 1)
  

Answer 1

Z3 is correct here; the script as you posed is indeed unsat. Here's what you said:

• Let there be two constants ss1 and ss3

• For all integers t_ss3 and t_ss1, whenever t_ss1 < t_ss3 holds, it must be the case that:

  • ss1 < ss3
  • AND, t_ss1 equals ss1
  • AND, t_ss3 equals ss3

This is clearly not true for all t_ss1 and t_ss3. There is no ss1 and ss3 that would satisfy this for ALL t_ss1 and t_ss2. You only need to look at the very last clause: You can't expect all t_ss3 to equal an arbitrary ss3.

I suspect you're trying to express some other property; but you did not code it correctly. Maybe you were trying to say if t_ss1 equals ss1 and t_ss3 equals ss3, and t_ss1 < t_ss3, then ss1 < ss3? That would be coded like the following:

(declare-const ss1 Int)
(declare-const ss3 Int)

(assert (forall ((t_ss3 Int) (t_ss1 Int))
        (=> (and (< t_ss1 t_ss3)
                 (= t_ss1 ss1)
                 (= t_ss3 ss3))
            (< ss1 ss3))))

(check-sat)

and would indeed produce sat.

If you come up with a better description of what you're trying to express, you can get better help in modeling it in SMT-Lib in a different question.