I found a soundness issue where z3-noodler returns unsat for a benchmark containing two independent constraints (one involving Real arithmetic with quantifiers, and another involving Strings).
Crucially, z3-noodler returns sat for each constraint when run in isolation. However, it incorrectly returns unsat when they are combined. Reference solvers like Z3 and cvc5 correctly return sat for the full benchmark.

(declare-const x Real)
(declare-const t String)
(assert (forall ((i Int)) (or (< i 0) (> i (to_int x)))))
(assert (> 1 (ite (str.< t ";") 1 0)))
(check-sat)

z3-noodler return unsat.
z3 / cvc5 return sat.
version:

Z3 version 4.15.1 - 64 bit 
- build hashcode 9274e4c8faa89ce4c46bb4c95a18ebf54040abbd 
- mata hashcode fe5ec3898a2bfbaebafcfa163b27bd4951cece0c