Refutational Soundness issue on QF_UFNIA

[depted]

Greetings,
For this instance, a refutational soundness bug occurred. Also, we checked that this instance should be "SAT". We truly hope that this instance will be helpful for the z3 team.

$ ./z3 ./small.smt2
unsat

$ cvc5 ./small.smt2
sat

$ cat ./small.smt2
(set-logic QF_UFNIA)
(declare-fun pow2 (Int) Int)
(define-fun bitof ((t Int) (l Int) (a Int)) Int (div a (pow2 l)))
(define-fun in_range ((k Int) (x Int)) Bool (and (> x 0) (< x (pow2 k))))
(define-fun intudivtotal ((t Int) (a Int) (b Int)) Int (ite false (pow2 0) (div a b)))
(define-fun intmodtotal ((s Int) (a Int) (b Int)) Int (ite false a (mod a b)))
(define-fun intlshr ((t Int) (a Int) (b Int)) Int (intmodtotal 0 (pow2 1) (intudivtotal 0 a (pow2 b))))
(define-fun intashr ((k Int) (a Int) (b Int)) Int (ite (= 0 (bitof 0 (- k 1) a)) (intlshr 0 a b) a))
(define-fun pow2_base_cases () Bool (= 1 (pow2 0)))
(define-fun pow2_ax () Bool pow2_base_cases)
(declare-fun k () Int)
(declare-fun s () Int)
(assert (in_range k s))
(assert (= 0 (mod (pow2 0) (ite false (pow2 0) (ite (= 0 (pow2 (intashr (+ 1 (div 0 s)) (- 4) k))) 1 0)))))
(assert pow2_ax)
(check-sat)

commit version: 53ca65a