(set-option :produce-models true)
(set-logic QF_UF)
(declare-sort U 0)
(declare-fun a () U)
(declare-fun b () U)
(declare-fun c () U)
(declare-fun f (U) U)
(declare-fun p () Bool)
(assert (=> p (= a b)))
(assert (=> p (= b c)))
(assert (=> p (not (= (f a) (f c)))))
(check-sat)
(push 1)
(assert p)
(check-sat)
(pop 1)
(check-sat)