search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.29k stars 1.48k forks source link

Memory leak on QF_NRA formula (opt) #4052

Closed rainoftime closed 4 years ago

rainoftime commented 4 years ago

Hi, for the following formula,

(set-logic QF_NRA)
(declare-const r2 Real)
(declare-const r3 Real)
(declare-const v4 Bool)
(assert (or v4 (> r3 8970947220.0 r3)))
(maximize (* 141897008.0 8970947220.0 141897008.0 141897008.0 r2))
(check-sat)

z3 commit dd064a5 throws a memory leak

==179177==ERROR: LeakSanitizer: detected memory leaks

Direct leak of 40 byte(s) in 1 object(s) allocated from:
    #0 0x7fa5052ba662 in malloc (/usr/lib/x86_64-linux-gnu/libasan.so.2+0x98662)
    #1 0x25ee7ab in memory::allocate(unsigned long) ../src/util/memory_manager.cpp:268
    #2 0x261e7b9 in small_object_allocator::allocate(unsigned long) ../src/util/small_object_allocator.cpp:103
    #3 0x26369b7 in mpz_manager<false>::allocate(unsigned int) ../src/util/mpz.cpp:198
    #4 0x263911f in mpz_manager<false>::big_set(mpz&, mpz const&) ../src/util/mpz.cpp:1498
    #5 0x562859 in mpz_manager<false>::set(mpz&, mpz const&) ../src/util/mpz.h:532
    #6 0x56428e in mpq_manager<false>::set(mpz&, mpz const&) ../src/util/mpq.h:660
    #7 0x563e40 in mpq_manager<false>::set(mpq&, mpq const&) ../src/util/mpq.h:663
    #8 0xd85216 in simplex::sparse_matrix<simplex::mpq_ext>::add_var(simplex::sparse_matrix<simplex::mpq_ext>::row, mpq const&, unsigned int) (/home/peisen/test/tofuzz/z3-debug/build/z3+0xd85216)
    #9 0xd7878d in simplex::simplex<simplex::mpq_ext>::add_row(unsigned int, unsigned int, unsigned int const*, mpq const*) ../src/math/simplex/simplex_def.h:47
    #10 0xd673e5 in smt::theory_diff_logic<smt::rdl_ext>::update_simplex(simplex::simplex<simplex::mpq_ext>&) (/home/peisen/test/tofuzz/z3-debug/build/z3+0xd673e5)
    #11 0xd5fdaf in smt::theory_diff_logic<smt::rdl_ext>::maximize(int, obj_ref<expr, ast_manager>&, bool&) (/home/peisen/test/tofuzz/z3-debug/build/z3+0xd5fdaf)
    #12 0x5c5f80 in opt::opt_solver::maximize_objective(unsigned int, obj_ref<expr, ast_manager>&) ../src/opt/opt_solver.cpp:242
    #13 0x5e6843 in opt::optsmt::geometric_lex(unsigned int, bool) ../src/opt/optsmt.cpp:220
    #14 0x5ead19 in opt::optsmt::lex(unsigned int, bool) ../src/opt/optsmt.cpp:502
    #15 0x57cf94 in opt::context::execute_min_max(unsigned int, bool, bool, bool) ../src/opt/opt_context.cpp:409
    #16 0x57d751 in opt::context::execute(opt::context::objective const&, bool, bool) ../src/opt/opt_context.cpp:435
    #17 0x57c0af in opt::context::optimize(ref_vector<expr, ast_manager> const&) ../src/opt/opt_context.cpp:332
    #18 0x19a1893 in cmd_context::check_sat(unsigned int, expr* const*) ../src/cmd_context/cmd_context.cpp:1527
    #19 0x193223b in smt2::parser::parse_check_sat() ../src/parsers/smt2/smt2parser.cpp:2596
    #20 0x19361d7 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2938
    #21 0x19378e9 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3130
    #22 0x19168ce in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3179
    #23 0x43c256 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:89
    #24 0x45440c in main ../src/shell/main.cpp:352
    #25 0x7fa50435782f in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x2082f)
rainoftime commented 4 years ago

Another test case

(set-logic QF_UFNRA)
(declare-fun _substvar_52_ () Bool)
(declare-const r1 Real)
(assert (or (xor true true true true true (>= 0.0 r1 0.0 0.0) true true) _substvar_52_))
(check-sat)
(check-sat)
(check-sat)
(minimize (* 7045497119.0 7045497119.0 r1 49460.0 7045497119.0))
(check-sat)