Performance on solve a logical problem about unexplained functions

[Heaven2024]

Hi! Z3 version 4.13.1 - 64 bit ubuntu:22.04

For the following cases：

(set-logic ALL)
(declare-sort S0 0)
(declare-fun g (S0) S0)
(declare-const s0 S0)
(declare-const s1 S0)
(assert (forall ((q1 S0))
    (exists ((q2 S0))
        (and (= (g (g q1)) (g q2)) (not (= (g s0) (g s1)))))))
(check-sat)
(get-model)

for Z3：

timeout  60s z3 test.smt2
z3 interrupted by SIGTERM. 

but it can be solved:

time cvc5 test.smt2 --produce-models --check-model
sat
(
; cardinality of S0 is 2
; rep: (as @S0_0 S0)
; rep: (as @S0_1 S0)
(define-fun g (($x1 S0)) S0 (ite (= (as @S0_0 S0) $x1) (as @S0_1 S0) (as @S0_0 S0)))
(define-fun s0 () S0 (as @S0_1 S0))
(define-fun s1 () S0 (as @S0_0 S0))
)
real    0m0.080s
user    0m0.035s
sys     0m0.045s

[NikolajBjorner]

smt.ematching=false