Statistics of two different Z3 runs involving reals

encodingA.z3stats

(:add-rows                3020
 :added-eqs               18032658
 :assert-diseq            618
 :assert-lower            1863166
 :assert-upper            1584866
 :bound-prop              12256
 :conflicts               219448
 :datatype-accessor-ax    36
 :datatype-constructor-ax 3824656
 :datatype-occurs-check   172432
 :datatype-splits         3007
 :decisions               4260689
 :del-clause              3022895
 :eq-adapter              1349661
 :final-checks            92275
 :fixed-eqs               237611
 :max-generation          13
 :memory                  9.43
 :minimized-lits          2322
 :mk-clause               3022895
 :pivots                  772
 :propagations            5734906
 :quant-instantiations    1748920
 :time                    42.78
 :total-time              52.43)

encodingB.z3stats

(:add-rows                8080739
 :added-eqs               17773617
 :arith-conflicts         26932
 :assert-diseq            1541
 :assert-lower            2276905
 :assert-upper            2026144
 :bound-prop              12796
 :conflicts               218801
 :datatype-accessor-ax    36
 :datatype-constructor-ax 3785071
 :datatype-occurs-check   170044
 :datatype-splits         3001
 :decisions               4248281
 :del-clause              2917176
 :eq-adapter              1345190
 :final-checks            114402
 :fixed-eqs               244155
 :grobner                 1448611
 :max-generation          13
 :max-min                 839556
 :memory                  10.79
 :minimized-lits          2322
 :mk-clause               2917176
 :nonlinear-horner        2603158
 :pivots                  713511
 :propagations            5619379
 :quant-instantiations    1635711
 :time                    660.25
 :total-time              676.66)