Memory leak on QF_NIA formula

[rainoftime]

Hi, for the following formula,

(set-logic QF_NIA)
(set-option :smt.arith.solver 1)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v9 Bool)
(declare-const v11 Bool)
(declare-const v12 Bool)
(declare-const v13 Bool)
(declare-const v14 Bool)
(declare-const v15 Bool)
(declare-const v16 Bool)
(declare-const v17 Bool)
(declare-const v18 Bool)
(declare-const i2 Int)
(declare-const i3 Int)
(declare-const v23 Bool)
(declare-const v29 Bool)
(declare-const i4 Int)
(push 1)
(assert (or v13 (<= 305 305 (* 749 (- 749 83 659) i2 (- 867 174 i2 (* (- 12 83) 202 (* (- 749 83 659) (- 12 83) 202 659) (* (- 749 83 659) (- 12 83) 202 659))) (- 867 174 i2 (* (- 12 83) 202 (* (- 749 83 659) (- 12 83) 202 659) (* (- 749 83 659) (- 12 83) 202 659)))) (- (* (- 749 83 659) (- 12 83) 202 659))) (and (not v0) v9 v16 v18 v11 v15)))
(assert (or (and v23 v12 v5 v18 v15 v5 v12) v2 v29))
(assert (and (or (and (not v0) v9 v16 v18 v11 v15) (<= 305 305 (* 749 (- 749 83 659) i2 (- 867 174 i2 (* (- 12 83) 202 (* (- 749 83 659) (- 12 83) 202 659) (* (- 749 83 659) (- 12 83) 202 659))) (- 867 174 i2 (* (- 12 83) 202 (* (- 749 83 659) (- 12 83) 202 659) (* (- 749 83 659) (- 12 83) 202 659)))) (- (* (- 749 83 659) (- 12 83) 202 659))) v17) (or v6 v29 (<= 305 305 (* 749 (- 749 83 659) i2 (- 867 174 i2 (* (- 12 83) 202 (* (- 749 83 659) (- 12 83) 202 659) (* (- 749 83 659) (- 12 83) 202 659))) (- 867 174 i2 (* (- 12 83) 202 0 (* 0 (- 12 83) 202 659)))) (- (* (- 749 83 659) (- 12 83) 202 659)))) (or v29 v13 (and (not v0) v9 v16 v18 v11 v15)) (or (and (not v0) v9 v16 v18 v11 v15) (> (- (* (- 749 83 659) (- 12 83) 202 659)) (- 12 83)) (and (not v0) v9 v16 v18 v11 v15)) (or v29 v6 v2) (or v6 v17 (<= 305 305 0 0)) (or (and (not v0) v9 v16 v18 v11 v15) (and (not v0) v9 v16 v18 v11 v15) (and v23 v12 v5 v18 v15 v5 v12)) (or v17 (<= 305 305 0 0) v17) (or (or v2 v17 (and (not v0) v9 v16 v18 v11 v15)) (or v2 v29 (and v23 v12 v5 v18 v15 v5 v12)) (or v13 (and v23 v12 v5 v18 v15 v5 v12) (<= 305 305 0 0)) (or (and (not v0) v9 v16 v18 v11 v15) (and (not v0) v9 v16 v18 v11 v15) (and v23 v12 v5 v18 v15 v5 v12)) (or v29 v13 (and (not v0) v9 v16 v18 v11 v15)) (or v13 (> (- 0) 0) (and v23 v12 v5 v18 v15 v5 v12)) (or (<= 305 305 (* 749 (- 749 83 659) i2 (- 867 174 i2 (* (- 12 83) 202 (* (- 749 83 659) (- 12 83) 202 659) (* (- 749 83 659) (- 12 83) 202 659))) (- 867 174 i2 (* (- 12 83) 202 (* (- 749 83 659) (- 12 83) 202 659) (* (- 749 83 659) (- 12 83) 202 659)))) 0) (and v23 v12 v5 v18 v15 v5 v12) (<= 305 305 0 0))) (or v6 v13 v17)))
(check-sat)
(assert (or (and (not v0) v9 v16 v18 v11 v15) v2 v13))
(check-sat)

z3 (commit 7f1b147) throws a leak when timemout

sat                                                                                                                                                                                               
sat

=================================================================
==182974==ERROR: LeakSanitizer: detected memory leaks

Direct leak of 160 byte(s) in 4 object(s) allocated from:
    #0 0x7fa418c2b662 in malloc (/usr/lib/x86_64-linux-gnu/libasan.so.2+0x98662)
    #1 0x25e3b35 in memory::allocate(unsigned long) ../src/util/memory_manager.cpp:268
    #2 0x2613b43 in small_object_allocator::allocate(unsigned long) ../src/util/small_object_allocator.cpp:103
    #3 0x262bd41 in mpz_manager<false>::allocate(unsigned int) ../src/util/mpz.cpp:198
    #4 0x262e4a9 in mpz_manager<false>::big_set(mpz&, mpz const&) ../src/util/mpz.cpp:1498
    #5 0x5627ad in mpz_manager<false>::set(mpz&, mpz const&) ../src/util/mpz.h:532
    #6 0x249fff1 in mpzzp_manager::set(mpz&, mpz const&) ../src/util/mpzzp.h:235
    #7 0x24af4e0 in polynomial::manager::imp::mk_linear(unsigned int, rational const*, unsigned int const*, rational const&) ../src/math/polynomial/polynomial.cpp:2665
    #8 0x249afec in polynomial::manager::mk_linear(unsigned int, rational const*, unsigned int const*, rational const&) ../src/math/polynomial/polynomial.cpp:7164
    #9 0x1f8b5ca in nlsat::solver::imp::search_check() ../src/nlsat/nlsat_solver.cpp:1578
    #10 0x1f8bf9b in nlsat::solver::imp::check() ../src/nlsat/nlsat_solver.cpp:1619
    #11 0x1f78239 in nlsat::solver::check() ../src/nlsat/nlsat_solver.cpp:3484
    #12 0x16a6bf1 in nlsat_tactic::imp::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/nlsat/tactic/nlsat_tactic.cpp:159
    #13 0x16a7740 in nlsat_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/nlsat/tactic/nlsat_tactic.cpp:241
    #14 0x1a65773 in cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:918
    #15 0x1a5e465 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
    #16 0x1a5e465 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
    #17 0x1a5e465 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
    #18 0x1a5e465 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120