Potential refutation soundness issue on UF formula

[rainoftime]

Hi, for this formula, yices a14eced

z3 xx.smt2
sat
yices_smt2 xx.smt2                                                                                 
unsat
$ cat xx.smt2
(set-logic UF)
(declare-sort S0 0)
(assert (not (exists ((q3 S0) (q4 S0) (q5 Bool) (q6 Bool) (q7 S0) (q8 Bool)) (=> (= q3 q4 q7) false))))
(check-sat)

[dddejan]

Simplified problem

(set-logic UF)
(declare-sort S0 0)
(assert (forall ((x S0) (y S0)) (= x y)))
(check-sat)
(get-model)

Output

$ z3 issue315.smt2; ./yices_smt2 issue315.smt2;
sat
(model 
  ;; universe for S0:
  ;;   S0!val!0 
  ;; -----------
  ;; definitions for universe elements:
  (declare-fun S0!val!0 () S0)
  ;; cardinality constraint:
  (forall ((x S0)) (= x S0!val!0))
  ;; -----------
)
unsat
(error "the context is unsatisfiable")

@aman-goel can you take a look

[aman-goel]

Resolved by db47e78 . Thanks!