uuverifiers
Inconsistent result for a simple satisfiability query
Consider the following smtlib satisfiability query:
; query.smt2
(set-logic UFLIA)
(declare-fun n () Int)
(assert (and (> n 1) (not (= (- n 1) 1))))
(check-sat)
(get-model)
corresponding to asking whether $n > 1 \land n \not = 2$ is satisfiable. $n = 3$ is a possible model.
Edit: a simpler query (assert (> n 1)) also works.
Running it through different solvers, one sees the outputs:
# running z3
▲ dotty/smt-sessions/eld-query z3 query.smt2
sat
(
(define-fun n () Int
3)
)
# running cvc5
▲ dotty/smt-sessions/eld-query cvc5 query.smt2 --produce-models
sat
(
(define-fun n () Int 3)
)
# running eldarica
▲ dotty/smt-sessions/eld-query eldarica -hsmt -scex query.smt2
Warning: ignoring get-model
unsat
0: false
Note that in the third command, the eldarica output differs from that of z3 and cvc5 on this query. Is this a bug or some expected difference in interpretation of the problem?
P.S.:
Changing the query to that of an equivalent transition system / predicate abstraction problem gets the right result:
; query.smt2
(set-logic UFLIA)
(declare-fun zero (Int) Bool)
(declare-fun one (Int) Bool)
(assert (forall ((x Int)) (zero x)))
(assert (forall ((x Int)) (=> (and (zero x) (> x 1)) (one x))))
(assert (forall ((x Int)) (=> (and (one x) (not (= x 2))) false)))
(check-sat)
Summary:
$$ \begin{align*} \top & \implies zero(x) \ zero(x) \land x > 1 & \implies one(x) \ one(x) \land x \not = 2 & \implies \bot \end{align*} $$
Solver outputs on predicate abstraction problem:
# cvc5
▲ dotty/smt-sessions/eld-query cvc5 query.smt2
unknown
# z3
▲ dotty/smt-sessions/eld-query z3 query.smt2
unsat
# eldarica
▲ dotty/smt-sessions/eld-query eldarica -hsmt -scex query.smt2
unsat
0: false -> 1
1: (one 3) -> 2
2: (zero 3)
That’s an interesting corner case. The right behavior for Eldarica should be to reject this input, since it is not a problem in Horn clause format, so outside of the fragment that Eldarica can handle. I need to look into why the SMT-LIB front-end does not correctly recognize that the input is ill-formed!
