Memoyr leak for QF_NRA insance (incremental solving)

[rainoftime]

Hi, for the following instance,
asan detects a memory leak issue in z3 commit 8717c7d

(declare-const v1 Bool)
(declare-const v3 Bool)
(declare-const r0 Real)
(declare-const r1 Real)
(assert (or v3 v1))
(check-sat)
(assert (= true true true (distinct 0.0 558186.674 r0 (* r0 25269393063.0 r1 558186.674 558186.674)) true true v1 true true true))
(check-sat)

=================================================================
==5174==ERROR: LeakSanitizer: detected memory leaks

Direct leak of 40 byte(s) in 1 object(s) allocated from:
    #0 0x7faf412de602 in malloc (/usr/lib/x86_64-linux-gnu/libasan.so.2+0x98602)
    #1 0x250b38f in memory::allocate(unsigned long) ../src/util/memory_manager.cpp:268
    #2 0x24cda7a in mpz_manager<true>::allocate(unsigned int) (/home/rainoftime/Work/tofuzz/z3/build/z3+0x24cda7a)
    #3 0x24d018f in mpz_manager<true>::big_set(mpz&, mpz const&) ../src/util/mpz.cpp:1497
    #4 0x47600b in mpz_manager<true>::set(mpz&, mpz const&) ../src/util/mpz.h:530
    #5 0x475cec in mpq_manager<true>::set(mpz&, mpz const&) ../src/util/mpq.h:653
    #6 0x474b08 in mpq_manager<true>::set(mpq&, mpq const&) ../src/util/mpq.h:656
    #7 0x4728bf in rational::rational(rational const&) ../src/util/rational.h:43
    #8 0x1353400 in std::pair<rational, expr*>::pair<expr*&, void>(rational const&, expr*&) /usr/include/c++/5/bits/stl_pair.h:139
    #9 0x1254f26 in smt::theory_arith<smt::mi_ext>::horner(unsigned int, old_sbuffer<std::pair<rational, expr*>, 16u>&, expr*) ../src/smt/theor
y_arith_nl.h:1496
    #10 0x12563e9 in smt::theory_arith<smt::mi_ext>::cross_nested(unsigned int, old_sbuffer<std::pair<rational, expr*>, 16u>&, expr*) ../src/sm
t/theory_arith_nl.h:1607
    #11 0x1256a24 in smt::theory_arith<smt::mi_ext>::is_cross_nested_consistent(old_sbuffer<std::pair<rational, expr*>, 16u>&) ../src/smt/theor
y_arith_nl.h:1629
    #12 0x1257a44 in smt::theory_arith<smt::mi_ext>::is_cross_nested_consistent(smt::theory_arith<smt::mi_ext>::row const&) ../src/smt/theory_a
rith_nl.h:1717
    #13 0x1257d5b in smt::theory_arith<smt::mi_ext>::is_cross_nested_consistent(old_svector<int, unsigned int> const&) ../src/smt/theory_arith_
nl.h:1731
    #14 0x1263d5c in smt::theory_arith<smt::mi_ext>::process_non_linear() ../src/smt/theory_arith_nl.h:2454
    #15 0x121f374 in smt::theory_arith<smt::mi_ext>::final_check_core() ../src/smt/theory_arith_core.h:1485
    #16 0x121fad0 in smt::theory_arith<smt::mi_ext>::final_check_eh() ../src/smt/theory_arith_core.h:1523
    #17 0xcee16b in smt::context::final_check() ../src/smt/smt_context.cpp:3902
    #18 0xced174 in smt::context::bounded_search() ../src/smt/smt_context.cpp:3818
    #19 0xcea8af in smt::context::search() ../src/smt/smt_context.cpp:3645
    #20 0xce8e37 in smt::context::check(unsigned int, expr* const*, bool) ../src/smt/smt_context.cpp:3530
    #21 0xcc38c6 in smt::kernel::imp::check(unsigned int, expr* const*) ../src/smt/smt_kernel.cpp:116
    #22 0xcc24ab in smt::kernel::check(unsigned int, expr* const*) ../src/smt/smt_kernel.cpp:296
    #23 0xecb426 in check_sat_core2 ../src/smt/smt_solver.cpp:190
    #24 0x196aaf5 in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67
    #25 0x1965646 in combined_solver::check_sat_core(unsigned int, expr* const*) ../src/solver/combined_solver.cpp:219
    #26 0x1962b83 in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:330

[NikolajBjorner]

duplicate of #3469