search

Z3Prover / z3

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

Memory leak for CHC(BV) formula (xform.fix_unbound_var, xform.bit_blast) #3905

Closed rainoftime closed 4 years ago

rainoftime commented 4 years ago

Related https://github.com/Z3Prover/z3/issues/3881

Hi, for the following formula

(set-logic HORN)
(set-option :fp.xform.fix_unbound_vars true)
(set-option :fp.xform.bit_blast true)
(assert (forall ((q42 (_ BitVec 27)) (q43 (_ BitVec 27)) (q44 (_ BitVec 27)) (q45 (_ BitVec 27)) (q46 (_ BitVec 27)) (q47 (_ BitVec 27)) (q48 (_ BitVec 27)) (q49 (_ BitVec 27)) (q50 (_ BitVec 27)) (q51 (_ BitVec 27)) (q52 (_ BitVec 10))) (=> (distinct ((_ rotate_right 5) q52) q52) (bvslt (_ bv0 27) q46))))
(assert (forall ((q53 (_ BitVec 27)) (q54 (_ BitVec 27)) (q55 (_ BitVec 27)) (q56 (_ BitVec 27)) (q57 (_ BitVec 27)) (q58 (_ BitVec 27)) (q59 (_ BitVec 27)) (q60 Bool)) (=> (xor q60 q60 q60 q60 q60 q60) (distinct (_ bv0 27) (bvsrem (_ bv0 27) q56)))))
(check-sat)

z3 commit d53e30e throws a memory leak

==39652==ERROR: LeakSanitizer: detected memory leaks                                                                                 [295/1876]

Direct leak of 256 byte(s) in 1 object(s) allocated from:
    #0 0x7fa2b43e6b90 in __interceptor_malloc (/usr/lib/x86_64-linux-gnu/libasan.so.4+0xdeb90)
    #1 0x2c438f1 in memory::allocate(unsigned long) ../src/util/memory_manager.cpp:268
    #2 0x2c43424 in memory::allocate(char const*, int, char const*, unsigned long) ../src/util/memory_manager.cpp:207
    #3 0xa9eb69 in datalog::mk_bit_blast::impl::operator()(datalog::rule_set const&) ../src/muz/transforms/dl_mk_bit_blast.cpp:279
    #4 0xa9b603 in datalog::mk_bit_blast::operator()(datalog::rule_set const&) ../src/muz/transforms/dl_mk_bit_blast.cpp:335
    #5 0xb6586b in datalog::rule_transformer::operator()(datalog::rule_set&) ../src/muz/base/dl_rule_transformer.cpp:88
    #6 0xb26651 in datalog::context::transform_rules(datalog::rule_transformer&) ../src/muz/base/dl_context.cpp:706
    #7 0xa9a54f in datalog::apply_default_transformation(datalog::context&) ../src/muz/transforms/dl_transforms.cpp:101
    #8 0x74f2e5 in spacer::dl_interface::query(expr*) ../src/muz/spacer/spacer_dl_interface.cpp:106
    #9 0xb283d5 in datalog::context::query(expr*) ../src/muz/base/dl_context.cpp:880
    #10 0x69e7dc in horn_tactic::imp::verify(expr*, ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&) ..
/src/muz/fp/horn_tactic.cpp:255
    #11 0x69e37b in horn_tactic::imp::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/muz/fp/horn_tactic.cpp:241
    #12 0x6a025f in horn_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/muz/fp/horn_tactic.cpp:405
    #13 0x1e982af in cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:915
    #14 0x1e86483 in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:148
    #15 0x1e86a11 in check_sat(tactic&, ref<goal>&, ref<model>&, labels_vec&, obj_ref<app, ast_manager>&, obj_ref<dependency_manager<ast_manag$
    #16 0x1e0f28a in check_sat_core2 ../src/solver/tactic2solver.cpp:185
    #17 0x1e0cba5 in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67
    #18 0x1e073d7 in combined_solver::check_sat_core(unsigned int, expr* const*) ../src/solver/combined_solver.cpp:246
    #19 0x1e0414d in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:330
    #20 0x1db3426 in cmd_context::check_sat(unsigned int, expr* const*) ../src/cmd_context/cmd_context.cpp:1581
    #21 0x1d31423 in smt2::parser::parse_check_sat() ../src/parsers/smt2/smt2parser.cpp:2596
    #22 0x1d3587c in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2938
    #23 0x1d37089 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3130
    #24 0x1d11010 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:
3179
    #25 0x46f7a1 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:89
    #26 0x459aac in main ../src/shell/main.cpp:352
agurfinkel commented 4 years ago

try with 136b0b23ce50285acbad20bca4a6eefbdaf39f9b

rainoftime commented 4 years ago

Fixed. Now the result is "unknown"