Possible bug in z3str3 (?)

[OrenGitHub]

Hi, I have the following simple unsat query for which z3 returns immediately with a correct answer. When I try it with smt.string_solver=z3str3, it hangs (for at least 10 mins before I kill it).

(declare-fun AB_serial_1_version_0 () String)
(declare-fun AB_serial_1_version_1 () String)

(assert (= (str.len AB_serial_1_version_0) 16))
(assert (= (str.len AB_serial_1_version_1) (str.len AB_serial_1_version_0)))
(assert (= (str.at AB_serial_1_version_1 15) (seq.unit #x00)))

(assert (= (str.indexof (str.substr AB_serial_1_version_1 0 (- 16 0)) (seq.unit #x00) 0) (- 0 1)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; if I use this instead, then both native z3                  ;
; and z3str3 return immediately with a (correct) unsat answer ;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;(assert (= (str.indexof AB_serial_1_version_1 (seq.unit #x00) 0) (- 0 1)))

(check-sat)

If I remove the substring component, both z3str3 and native z3 (is that a good name?) return immediately with a correct unsat answer. What's going on here? Is this related somehow to #1397 ? Thanks!

[NikolajBjorner]

Perhaps this is for @mtrberzi

[mtrberzi]

Thanks -- taking a look

[NikolajBjorner]

still diverges

[mtrberzi]

Still diverges but I'm curious about how z3str3 should interact with seq.unit here