`ostrich` returns `sat` for an `unsat` formula with quantification

[wingsyuyi-satori]

I found a soundness bug in ostrich when solving a very simple formula with quantifiers. The formula is as follows:

(set-logic ALL)
(assert
  (forall ((char String))
    (=> (str.contains char ":")
        (str.contains char "://"))))
(check-sat)

The meaning of this formula is: for all strings, if a string contains ":", then it must also contain "://".
This formula is clearly unsatisfiable, since there exists a counterexample (e.g., the string ":").
z3 correctly returns unsat for this input, while ostrich returns sat.
The ostrich version used is:

ostrich +version
2025-11-17