Incorrect handling of str.replace_re

[pruemmer]

For this input, Ostrich reports unsat, cvc5 sat:

(define-fun sigmaStar_048 () String "Ajavascript:")
(define-fun b_sigmaStar_048 () Bool true)
(define-fun literal_9 () String "\u{5c}x3c\u{5c}x74\u{5c}x64\u{5c}x3e\u{5c}x55\u{5c}x52\u{5c}x4c\u{5c}x3a\u{5c}x20")
(define-fun b_literal_9 () Bool true)
(define-fun literal_11 () String "\u{5c}x3c\u{5c}x2f\u{5c}x74\u{5c}x64\u{5c}x3e")
(define-fun b_literal_11 () Bool true)
(define-fun atkPtn () String "javascript:")
(define-fun b_atkPtn () Bool false)
(define-fun x_7 () String "javascript:")
(define-fun b_x_7 () Bool true)
(define-fun x_10 () String "\u{5c}x3c\u{5c}x74\u{5c}x64\u{5c}x3e\u{5c}x55\u{5c}x52\u{5c}x4c\u{5c}x3a\u{5c}x20javascript:")
(define-fun b_x_10 () Bool true)
(define-fun x_12 () String "\u{5c}x3c\u{5c}x74\u{5c}x64\u{5c}x3e\u{5c}x55\u{5c}x52\u{5c}x4c\u{5c}x3a\u{5c}x20javascript:\u{5c}x3c\u{5c}x2f\u{5c}x74\u{5c}x64\u{5c}x3e")
(define-fun b_x_12 () Bool true)
(define-fun sink () String "\u{5c}x3c\u{5c}x74\u{5c}x64\u{5c}x3e\u{5c}x55\u{5c}x52\u{5c}x4c\u{5c}x3a\u{5c}x20javascript:\u{5c}x3c\u{5c}x2f\u{5c}x74\u{5c}x64\u{5c}x3e")
(define-fun b_sink () Bool false)
(define-fun atk_sigmaStar_1 () String "\u{5c}x3c\u{5c}x74\u{5c}x64\u{5c}x3e\u{5c}x55\u{5c}x52\u{5c}x4c\u{5c}x3a\u{5c}x20")
(define-fun atk_sigmaStar_2 () String "\u{5c}x3c\u{5c}x2f\u{5c}x74\u{5c}x64\u{5c}x3e")
(define-fun atk_sink () String "\u{5c}x3c\u{5c}x74\u{5c}x64\u{5c}x3e\u{5c}x55\u{5c}x52\u{5c}x4c\u{5c}x3a\u{5c}x20javascript:\u{5c}x3c\u{5c}x2f\u{5c}x74\u{5c}x64\u{5c}x3e")

(assert (= x_7 (str.replace_re sigmaStar_048 re.allchar "") ) )

(check-sat)