Closed
Description
Regular expression intersection for ranges of characters doesn't work the way I'd expect it to as of about a week ago:
In particular, the following:
(push)
(assert (str.in.re "p" (re.range "m" "r")))
(assert (str.in.re "p" (re.range "p" "z")))
(check-sat)
(pop)
(push)
(assert (not (str.in.re "p" (re.inter (re.range "p" "z") (re.range "m" "r")))))
(check-sat)
(pop)
(push)
(assert (str.in.re "p" (re.inter (re.range "p" "z") (re.range "m" "r"))))
(check-sat)
(pop)
Returns:
sat
sat
sat
I'd expect it to return (as p is in [p-z]&&[m-r], and similar to CVC4):
sat
unsat
sat
Am I right that this is a bug?
Metadata
Assignees
Labels
No labels