Hello, I found a case where OSTRICH solves two equisatisfiable SMT-LIB differently. They are shortened from a longer version, which cvc5 1.3.1 and I agree is sat, but OSTRICH thinks is unsat. The permalinks and the original version of the .smt2 file are below.
474.smt2
; https://eldarica.org/ostrich/?ex=perma%2F1765160376_1015288222 # sat
; https://eldarica.org/ostrich/?ex=perma%2F1765160439_463925 # unsat