Inconsistent satisfiability between Z3's "ctx-solver-simplify" and "ctx-simplify"

Question

I'm trying to make z3 (I'm using z3py) to check whether a formula is satisfiable or not and if it is satisfiable then simplify it.

I initially used Z3's ctx-solver-simplify. However, since I am repeatedly making many calls, using this tactic turns out to very expensive. So, instead I am trying to use Z3's ctx-simplify which only performs local simplifications but it should still return whether it is satisfiable or not.

However, I have run into a couple of situtations where it produces a simplification but it is NOT satisfiable. For example consider the following:

(declare-const x Int)
(declare-const y Int)
(assert (and (< x 6) (and (not (> x 2)) (and (= x y) (and (not (< x 8)) (not (= x 4)))))))
(apply (then ctx-solver-simplify propagate-values (par-then (repeat (or-else split-clause skip)) propagate-ineqs)))
(apply (then ctx-simplify propagate-values (par-then (repeat (or-else split-clause skip)) propagate-ineqs)))

Using ctx-solver-simplify return unsatisifiable whereas ctx-simplify returns a list of goals (shown below), thus satisfiable (which is clearly incorrect).

(goal
  (< x 6)
  (not (> x 2))
  (= x y)
  (not (< x 8))
  (not (= x 4))
  :precision precise :depth 2)
)

Could anyone please explain to me why this is happening and whether I am using the tactics correctly? Thanks!

Nuno Lopes Nuno Lopes · Accepted Answer · 2019-12-30T16:19:35

These tactics can return goals even if the formulas aren't satisfiable. Only tactics like smt (and tactics that call smt for you, like qfbv) won't do that. You can append 'smt' to your tactic pipeline.

Inconsistent satisfiability between Z3's "ctx-solver-simplify" and "ctx-simplify"

1 Answers