Inconsistent result for a simple satisfiability query

[sankalpgambhir]

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)

[pruemmer]

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!

[pruemmer]

This input is now rejected with an error.

[sankalpgambhir]

Thanks! I can confirm that this is rejected on the main branch.