Performance regression from 4.8.7.0 to 4.8.8.0 and all later versions.

[vrthra]

The following SMT queries get evaluated in less than a second in 4.8.7.0 but takes a long time in 4.8.8.0 and later.

(declare-const db_select_s_str_1 String)
(assert (let ((a!1 (not (<= (str.indexof (str.substr db_select_s_str_1 7 19)
                                 " where "
                                 0)
                    0))))
(let ((a!2 (or a!1
               (= 0
                  (str.indexof (str.substr db_select_s_str_1 7 19) " where " 0)))))
  (and (= 0 (str.indexof db_select_s_str_1 "select " 0))
       (<= 0 (str.indexof (str.substr db_select_s_str_1 7 19) " from " 0))
       (not a!2)
       (= (str.substr (str.substr db_select_s_str_1 7 19) 10 9) "inventory")))))
(check-sat)
(get-model)

(declare-const my_fn_a_int_1 Int)
(declare-const my_fn_b_int_2 Int)
(assert (let ((a!1 (bvnot (bvor (bvnot ((_ int2bv 64) my_fn_a_int_1))
                        (bvnot ((_ int2bv 64) my_fn_b_int_2))))))
(let ((a!2 (bvor (bvnot (bvor ((_ int2bv 64) my_fn_a_int_1)
                              ((_ int2bv 64) my_fn_b_int_2)))
                 a!1)))
  (not (= 0 (bv2int (bvnot a!2)))))))
(check-sat)
(get-model)

In 4.8.7.0, I get the following results immediately.

$ time ./bin/z3 a.smt
sat
(model 
  (define-fun db_select_s_str_1 () String
    "select  \x08 from \x00\x00inventory")
)
./bin/z3 a.smt  0.98s user 0.02s system 93% cpu 1.070 total
$ time ./bin/z3 b.smt
sat
(model 
  (define-fun my_fn_a_int_1 () Int
    (- 18446744073709551617))
  (define-fun my_fn_b_int_2 () Int
    (- 2))
)
./bin/z3 b.smt  3.27s user 0.03s system 97% cpu 3.393 total