Refutation Unsoundness -- Regex

[mrkmarron]

Maybe related to something in issue #5467 but I didn't see a direct duplicate. The following returns unsat when there is a very trivial satisfying solution. I have uncommented out a few variations I tried that do/do not change the sat/unsat result.

From my playing around it looks like the nested re++ has something to do with it. It checked both master head and release 4.8.12.

(set-logic ALL)

(declare-const _@@cons_String_entrypoint String)
(assert (<= (str.len _@@cons_String_entrypoint) 255))

(define-const _@@cons_StringOf_ForecastDetail__entrypoint Bool
    (str.in.re _@@cons_String_entrypoint (re.++ 
    (re.union (str.to.re "Showers") (str.to.re "Thunderstorms") (str.to.re "Snow") (str.to.re "Fog"))
    ;;[SAT](re.opt (re.union (str.to.re "Showers") (str.to.re "Thunderstorms") (str.to.re "Snow") (str.to.re "Fog")))))
    ;;[UNSAT](re.++ (str.to.re " And ") (str.to.re "Fog"))))
    ;;[UNSAT](re.++ (str.to.re " And ") (re.union (str.to.re "Showers") (str.to.re "Thunderstorms") (str.to.re "Snow") (str.to.re "Fog")))))
    (re.opt (re.++ (str.to.re " And ") (re.union (str.to.re "Showers") (str.to.re "Thunderstorms") (str.to.re "Snow") (str.to.re "Fog"))))))
)

(assert _@@cons_StringOf_ForecastDetail__entrypoint)

(check-sat)

[NikolajBjorner]

fixed with 6f55971