[691] % z3 t1.smt2 
unsat
[692] % z3 t2.smt2 
sat
[693] % cvc4 -q t1.smt2 
unsat
[694] % cvc4 -q t2.smt2 
(error "The logic was specified as AUFNIRA, which doesn't include THEORY_DATATYPES, but found a term in that theory.
You might want to extend your logic to AUFDTNIRA
")
[695] % 
[695] % cat t1.smt2 
(declare-datatypes ((S 0)) (((A))))
(declare-const x S)
(declare-const y S)
(assert (distinct x y))
(check-sat)
[696] % 
[696] % cat t2.smt2 
(set-logic AUFNIRA)
(declare-datatypes ((S 0)) (((A))))
(declare-const x S)
(declare-const y S)
(assert (distinct x y))
(check-sat)
[697] %