Long strings timeout

[orinatic]

Given the solver: (set-info :status unknown) (declare-fun full_string () String) (declare-fun string_contents () String) (declare-fun length_constraint () Int) (assert (= (str.indexof full_string "\x00" 0) (- (str.len full_string) 1))) (assert (let ((?x1087 (str.substr full_string 0 (- (str.len full_string) 1)))) (= string_contents ?x1087))) (assert (let ((?x1087 (str.substr full_string 0 (- (str.len full_string) 1)))) (not (str.contains ?x1087 "\x00")))) (assert (let ((?x1057 (+ 140145453959712 (str.indexof full_string "start" 0)))) (let (($x1058 (>= (str.indexof full_string "start" 0) 0))) (let ((?x1059 (ite $x1058 ?x1057 0))) (let ((?x1064 (+ 140145453959712 (str.indexof full_string "end" 0)))) (let (($x1065 (>= (str.indexof full_string "end" 0) 0))) (let ((?x1066 (ite $x1065 ?x1064 0))) (= length_constraint (+ ?x1066 (* (- 1) ?x1059)))))))))) (assert (> length_constraint 100)) (assert (let ((?x1099 (str.len full_string))) (>= ?x1099 length_constraint))) (assert (str.in.re string_contents (re.* (re.range ":" "}")))) (check-sat) (get-model)

z3 (from the command line) finishes in ~6 seconds. However, if I change the desired length to 500 (assert (> length_constraint 500)) it hangs (Runs for > 10 minutes)

Do you have any advice on what's going on here/any settings to toggle to make string solving more linear, or is this a lost cause as the desired length gets bigger?

Thank you!

[pjljvandelaar]

Have you also tried with the z3str3 solver? Pass smt.string_solver=z3str3 on the command line.