Optimization (soft assertion) solving slow after (reset)

[BillHallahan]

Using the (reset) command seems to sometimes cause Z3 (release version 4.8.17) to solve optimization problems significantly slower than it is otherwise able to. fast.txt and slow.txt are two SMT formulas:
fast.txt

slow.txt

fast.txt is a single problem involving both hard and soft assertions. Z3 can solve this in around 2.5s on my computer. slow.txt is the same as fast.txt, but with this:

(declare-const f_0_spr_1_0_c_coeff_act_1 Bool)
(declare-const f_0_sp_4_r_c_1_t_2_a_1 Int)


(assert-soft f_0_spr_1_0_c_coeff_act_1 :id minimal_size)
(assert-soft (and (<= (- 1) f_0_sp_4_r_c_1_t_2_a_1) (<= f_0_sp_4_r_c_1_t_2_a_1 1)) :id coeff)
(check-sat)
(get-info :all-statistics)

(reset)

added to the beginning of the file. However, Z3 then takes roughly 16s to solve the second problem, despite the call to (reset) (which should, as I understand, completely clear the state of the solver.)

Here is the full output from running fast.txt:

sat
(:added-eqs                   649859
 :arith-eq-adapter            3132
 :arith-bound-propagations-lp 11154
 :arith-branch                1
 :arith-conflicts             302
 :arith-cube-calls            1
 :arith-diseq                 362832
 :arith-fixed-eqs             2501
 :arith-gcd-calls             8
 :arith-gomory-cuts           2
 :arith-hnf-calls             1
 :arith-lower                 353965
 :arith-make-feasible         66661
 :arith-max-columns           458
 :arith-max-rows              335
 :arith-offset-eqs            187849
 :arith-patches               8
 :arith-patches-success       5
 :arith-upper                 386297
 :binary-propagations         1654515
 :bv-bit2core                 131
 :bv-dynamic-diseqs           548
 :bv->core-eq                 299
 :conflicts                   17443
 :decisions                   82598
 :del-clause                  11599
 :final-checks                153
 :max-memory                  57.28
 :maxsat-cores                23
 :memory                      57.04
 :minimized-lits              90794
 :mk-bool-var                 12626
 :mk-clause                   44211
 :num-allocs                  4514609
 :num-checks                  306
 :propagations                3971242
 :restarts                    95
 :rlimit-count                21697328
 :time                        2.56)

and from running slow.txt:

sat
(:arith-assert-lower  3
 :arith-assert-upper  3
 :binary-propagations 6
 :decisions           2
 :del-clause          2
 :final-checks        3
 :max-memory          39.02
 :memory              39.02
 :mk-bool-var         7
 :mk-clause           5
 :num-allocs          34660
 :num-checks          3
 :propagations        9
 :rlimit-count        630
 :time                0.01)
sat
(:added-eqs                   1958392
 :arith-eq-adapter            1640
 :arith-bound-propagations-lp 20937
 :arith-conflicts             371
 :arith-diseq                 1367604
 :arith-fixed-eqs             33059
 :arith-gcd-calls             2
 :arith-lower                 1104870
 :arith-make-feasible         214184
 :arith-max-columns           457
 :arith-max-rows              334
 :arith-offset-eqs            998329
 :arith-patches               2
 :arith-patches-success       2
 :arith-upper                 1486561
 :binary-propagations         8010253
 :bv-bit2core                 182
 :bv-dynamic-diseqs           898
 :bv->core-eq                 408
 :conflicts                   89230
 :decisions                   189254
 :del-clause                  30365
 :final-checks                190
 :max-memory                  87.26
 :maxsat-cores                22
 :memory                      87.12
 :minimized-lits              1006766
 :mk-bool-var                 8489
 :mk-clause                   120207
 :num-allocs                  17353753
 :num-checks                  361
 :propagations                18610953
 :restarts                    666
 :rlimit-count                94242860
 :time                        16.00)