BMC check satisfiable but can not print counterexample

[zhaoxuying]

The btor2 file is generated by Yosys，Since the DUT has an initialization time of approximately more than 1000 cycles, the command "sim -clock clock -resetn reset_n -n 1131 -rstlen 50 -zinit -w -fst xs_formal.fst top" is used in the yosys script. When the command "pono -v 3 -k 50 -e bmc --vcd xs-trace.vcd ./xs.btor2" is executed, the program stops here and it seems to be stuck in counterexample generation. Could you please provide some debugging suggestions? Thank you.