Common Subexpression prevents efficient solving

[BillHallahan]

The below SMT query:

(set-logic ALL)
(declare-const ds1_n__7566047373982660248 String)
(declare-const i_n__6989586621679031774 Int)
(declare-const fs_n__6989586621679195639 String)
(assert (= (str.len fs_n__6989586621679195639) 1))
(declare-const c_n__7566047373982604919 String)
(assert (= (str.len c_n__7566047373982604919) 1))
(declare-const $inspos_n__2 Int)
(declare-const ds1_n__7566047373982660247 String)
(declare-const fs_n__6989586621679195626 String)
(declare-const c_n__7566047373982604911 String)
(assert (= (str.len c_n__7566047373982604911) 1))
(declare-const ds2_n__7205759403793019315 String)
(declare-const c_n__7566047373982604918 String)

(assert (= (str.len c_n__7566047373982604918) 1))
(assert (= (str.++ c_n__7566047373982604919 ds2_n__7205759403793019315) (str.at (str.++ c_n__7566047373982604911 ds1_n__7566047373982660247) 3)))
(assert (forall ((i_n__6989586621679031774 Int))(=> (and (<= 0 i_n__6989586621679031774) (< i_n__6989586621679031774 $inspos_n__2)) (str.< (str.at (str.++ c_n__7566047373982604911 ds1_n__7566047373982660247) i_n__6989586621679031774) (str.++ fs_n__6989586621679195639 "")))))
(assert (or (= $inspos_n__2 (str.len (str.++ c_n__7566047373982604911 ds1_n__7566047373982660247))) (str.<= (str.++ fs_n__6989586621679195639 "") (str.at (str.++ c_n__7566047373982604911 ds1_n__7566047373982660247) $inspos_n__2))))
(assert (= (str.++ c_n__7566047373982604918 ds1_n__7566047373982660248) (str.++ (str.++ (str.substr (str.++ c_n__7566047373982604911 ds1_n__7566047373982660247) 0 $inspos_n__2) (str.++ fs_n__6989586621679195639 "")) (str.substr (str.++ c_n__7566047373982604911 ds1_n__7566047373982660247) $inspos_n__2 (str.len (str.++ c_n__7566047373982604911 ds1_n__7566047373982660247))))))
(assert (= (str.++ c_n__7566047373982604911 ds1_n__7566047373982660247) fs_n__6989586621679195626))
(assert (not (< (str.len fs_n__6989586621679195626) 9)))
(assert (= (str.at (str.++ (str.++ (str.substr (str.++ c_n__7566047373982604911 ds1_n__7566047373982660247) 0 $inspos_n__2) (str.++ fs_n__6989586621679195639 "")) (str.substr (str.++ c_n__7566047373982604911 ds1_n__7566047373982660247) $inspos_n__2 (str.len (str.++ c_n__7566047373982604911 ds1_n__7566047373982660247)))) 3) ""))
(assert (not (not (= c_n__7566047373982604911 c_n__7566047373982604918))))
(assert (= (+ (str.len (str.++ c_n__7566047373982604911 ds1_n__7566047373982660247)) 1) (str.len (str.++ (str.++ (str.substr (str.++ c_n__7566047373982604911 ds1_n__7566047373982660247) 0 $inspos_n__2) (str.++ fs_n__6989586621679195639 "")) (str.substr (str.++ c_n__7566047373982604911 ds1_n__7566047373982660247) $inspos_n__2 (str.len (str.++ c_n__7566047373982604911 ds1_n__7566047373982660247)))))))
(assert (not (= fs_n__6989586621679195626 "")))

(check-sat)

takes Z3 4.15.2 around 20s (on my system.) If it is rewritten to store the commonly appearing subexpression (str.++ c_n__7566047373982604911 ds1_n__7566047373982660247) in a variable:

(set-logic ALL)
(declare-const ds1_n__7566047373982660248 String)
(declare-const i_n__6989586621679031774 Int)
(declare-const fs_n__6989586621679195639 String)
(assert (= (str.len fs_n__6989586621679195639) 1))
(declare-const c_n__7566047373982604919 String)
(assert (= (str.len c_n__7566047373982604919) 1))
(declare-const $inspos_n__2 Int)
(declare-const ds1_n__7566047373982660247 String)
(declare-const fs_n__6989586621679195626 String)
(declare-const c_n__7566047373982604911 String)
(assert (= (str.len c_n__7566047373982604911) 1))
(declare-const ds2_n__7205759403793019315 String)
(declare-const c_n__7566047373982604918 String)

(declare-const j String)
(assert (= j (str.++ c_n__7566047373982604911 ds1_n__7566047373982660247)))

(assert (= (str.len c_n__7566047373982604918) 1))
(assert (= (str.++ c_n__7566047373982604919 ds2_n__7205759403793019315) (str.at j 3)))
(assert (forall ((i_n__6989586621679031774 Int))(=> (and (<= 0 i_n__6989586621679031774) (< i_n__6989586621679031774 $inspos_n__2)) (str.< (str.at j i_n__6989586621679031774) (str.++ fs_n__6989586621679195639 "")))))
(assert (or (= $inspos_n__2 (str.len j)) (str.<= (str.++ fs_n__6989586621679195639 "") (str.at j $inspos_n__2))))
(assert (= (str.++ c_n__7566047373982604918 ds1_n__7566047373982660248) (str.++ (str.++ (str.substr j 0 $inspos_n__2) (str.++ fs_n__6989586621679195639 "")) (str.substr j $inspos_n__2 (str.len j)))))
(assert (= j fs_n__6989586621679195626))
(assert (not (< (str.len fs_n__6989586621679195626) 9)))
(assert (= (str.at (str.++ (str.++ (str.substr j 0 $inspos_n__2) (str.++ fs_n__6989586621679195639 "")) (str.substr j $inspos_n__2 (str.len j))) 3) ""))
(assert (not (not (= c_n__7566047373982604911 c_n__7566047373982604918))))
(assert (= (+ (str.len j) 1) (str.len (str.++ (str.++ (str.substr j 0 $inspos_n__2) (str.++ fs_n__6989586621679195639 "")) (str.substr j $inspos_n__2 (str.len j))))))
(assert (not (= fs_n__6989586621679195626 "")))

(check-sat)

Z3 terminates with unsat almost instantly (0.03s).

It's surprising to me that there is such a large difference in solving time between these two formulas. Does Z3 support anything similar to common subexpression elimination (perhaps via a flag) that could help here?