1 2 3 4 5 6 7 8 9 10 11 12 13
; COMMAND-LINE: --strings-exp ; EXPECT: unsat (set-logic ALL) (declare-fun a () String) (declare-fun b () String) (assert (str.in_re a (re.range "a" "c"))) (assert (str.in_re a (re.* (re.union (re.++ (re.union (str.to_re "a") (str.to_re "b")) (str.to_re "a")) (str.to_re (str.from_int (str.len b))))))) (check-sat)