Response changes from Sat to Unsat if using set-simplifier

[facundominguez]

The following query changes the response from Sat to Unsat if we use set-simplifier.

I bumped into this after trying to apply the advice in #7770. I would expect any sort of simplification to not change the response of the solver. Is this a bug?

Thanks in advance!

z3 version: 4.15.1

; Uncommenting the line below changes the result of the third check-sat
;(set-simplifier (then simplify solve-eqs simplify))
(declare-datatypes ((Peano 0)) (((S (S$1 Peano)) (Z))))
(declare-fun ds_dRA () Peano)
(declare-fun dRN () Peano)

(assert (= dRN (S ds_dRA)))
(push 1)
(check-sat)
; SMT Says: Sat
(pop 1)
(push 1)
(assert (not (is-Z dRN)))
(check-sat)
; SMT Says: Sat
(pop 1)
(push 1)
(assert (is-Z dRN))
(check-sat)
; SMT Says: Sat