Memory Leak about sat.lookahead.delta_fraction

[Heaven2024]

Hi
Z3 [version 4.13.1 - 64 bit].
ubuntu:22.04
for this case:

(set-logic QF_FPBV)
(declare-fun x () (_ FloatingPoint 11 53))
(declare-fun y () (_ BitVec 64))
(assert (fp.gt x ((_ to_fp 11 53) RNE 1.0)))
(assert (bvult y #x8000000000000000))
(check-sat)

z3 test.smt2 
sat

When (set-option:sat.lookahead.delta_fraction 0.3) is added, a memory leak will be triggered

(set-option :sat.lookahead.delta_fraction 0.3)
(set-logic QF_FPBV)
(declare-fun x () (_ FloatingPoint 11 53))
(declare-fun y () (_ BitVec 64))
(assert (fp.gt x ((_ to_fp 11 53) RNE 1.0)))
(assert (bvult y #x8000000000000000))
(check-sat)

z3 test.smt2 
unknown

=================================================================
==2725223==ERROR: LeakSanitizer: detected memory leaks

Direct leak of 4408 byte(s) in 1 object(s) allocated from:
    #0 0x55d2b09eb36e in malloc (/yuhao/z3/build/z3+0x28436e) (BuildId: 5c00c5286df32e49d27f99f213a657243f3d2f76)
    #1 0x55d2b5f0ec95 in memory::allocate(unsigned long) /yuhao/z3/build/../src/util/memory_manager.cpp:301:16

SUMMARY: AddressSanitizer: 4408 byte(s) leaked in 1 allocation(s).

I also found that when the value of the option is set to 0.1/0.2, normal solving will not trigger the vulnerability.

[Heaven2024]

Similar situation, I think it is the reason of option itself

(set-option :sat.lookahead.delta_fraction 0.4)

(set-logic QF_BV)
(check-sat)

z3 test2.smt2
(error "line 4 column 10: invalid value for delta fraction. It should be a number in the interval 0 to 1")

=================================================================
==2806344==ERROR: LeakSanitizer: detected memory leaks

Direct leak of 5256 byte(s) in 3 object(s) allocated from:
    #0 0x555d31cf036e in malloc (/yuhao/z3/build/z3+0x28436e) (BuildId: 5c00c5286df32e49d27f99f213a657243f3d2f76)
    #1 0x555d37213c95 in memory::allocate(unsigned long) /yuhao/z3/build/../src/util/memory_manager.cpp:301:16

Indirect leak of 146232 byte(s) in 528 object(s) allocated from:
    #0 0x555d31cf036e in malloc (/yuhao/z3/build/z3+0x28436e) (BuildId: 5c00c5286df32e49d27f99f213a657243f3d2f76)
    #1 0x555d37213c95 in memory::allocate(unsigned long) /yuhao/z3/build/../src/util/memory_manager.cpp:301:16

Indirect leak of 22 byte(s) in 1 object(s) allocated from:
    #0 0x555d31d2acad in operator new(unsigned long) (/yuhao/z3/build/z3+0x2becad) (BuildId: 5c00c5286df32e49d27f99f213a657243f3d2f76)
    #1 0x555d31d53ba6 in void std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char>>::_M_construct<char const*>(char const*, char const*, std::forward_iterator_tag) /usr/lib/gcc/x86_64-linux-gnu/11/../../../../include/c++/11/bits/basic_string.tcc:219:14
    #2 0x555d31d53ba6 in std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char>>::basic_string<std::allocator<char>>(char const*, std::allocator<char> const&) /usr/lib/gcc/x86_64-linux-gnu/11/../../../../include/c++/11/bits/basic_string.h:539:2
    #3 0x555d31d53ba6 in qi_params::qi_params(params_ref const&) /yuhao/z3/build/../src/smt/params/qi_params.h:81:9
    #4 0x555d31d4ff8e in smt_params::smt_params(params_ref const&) /yuhao/z3/build/../src/smt/params/smt_params.h:253:5
    #5 0x555d3325a8b3 in smt_tactic::smt_tactic(ast_manager&, params_ref const&) /yuhao/z3/build/../src/smt/tactic/smt_tactic_core.cpp:52:5
    #6 0x555d3325a126 in mk_seq_smt_tactic(ast_manager&, params_ref const&) /yuhao/z3/build/../src/smt/tactic/smt_tactic_core.cpp:409:12
    #7 0x555d3325a126 in mk_smt_tactic_core(ast_manager&, params_ref const&, symbol const&) /yuhao/z3/build/../src/smt/tactic/smt_tactic_core.cpp:419:78
    #8 0x555d3227dfd1 in mk_smt_tactic(ast_manager&, params_ref const&) /yuhao/z3/build/../src/tactic/smtlogics/smt_tactic.cpp:30:12
    #9 0x555d322832b6 in mk_qfbv_tactic(ast_manager&, params_ref const&) /yuhao/z3/build/../src/tactic/smtlogics/qfbv_tactic.cpp:128:42
    #10 0x555d3226b688 in smt_strategic_solver_factory::operator()(ast_manager&, params_ref const&, bool, bool, bool, symbol const&) /yuhao/z3/build/../src/tactic/portfolio/smt_strategic_solver.cpp:181:17
    #11 0x555d35318dee in cmd_context::mk_solver() /yuhao/z3/build/../src/cmd_context/cmd_context.cpp:2244:16
    #12 0x555d35320039 in cmd_context::init_manager_core(bool) /yuhao/z3/build/../src/cmd_context/cmd_context.cpp:862:9
    #13 0x555d3523e93f in cmd_context::m() const /yuhao/z3/build/../src/cmd_context/cmd_context.h:412:63
    #14 0x555d3523e93f in smt2::parser::m() const /yuhao/z3/build/../src/parsers/smt2/smt2parser.cpp:123:48
    #15 0x555d3523e93f in smt2::parser::expr_stack() /yuhao/z3/build/../src/parsers/smt2/smt2parser.cpp:242:32
    #16 0x555d3523e93f in smt2::parser::parse_check_sat() /yuhao/z3/build/../src/parsers/smt2/smt2parser.cpp:2631:29

Indirect leak of 22 byte(s) in 1 object(s) allocated from:
    #0 0x555d31d2acad in operator new(unsigned long) (/yuhao/z3/build/z3+0x2becad) (BuildId: 5c00c5286df32e49d27f99f213a657243f3d2f76)
    #1 0x555d31d53ba6 in void std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char>>::_M_construct<char const*>(char const*, char const*, std::forward_iterator_tag) /usr/lib/gcc/x86_64-linux-gnu/11/../../../../include/c++/11/bits/basic_string.tcc:219:14
    #2 0x555d31d53ba6 in std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char>>::basic_string<std::allocator<char>>(char const*, std::allocator<char> const&) /usr/lib/gcc/x86_64-linux-gnu/11/../../../../include/c++/11/bits/basic_string.h:539:2
    #3 0x555d31d53ba6 in qi_params::qi_params(params_ref const&) /yuhao/z3/build/../src/smt/params/qi_params.h:81:9
    #4 0x555d31d4ff8e in smt_params::smt_params(params_ref const&) /yuhao/z3/build/../src/smt/params/smt_params.h:253:5
    #5 0x555d3325a8b3 in smt_tactic::smt_tactic(ast_manager&, params_ref const&) /yuhao/z3/build/../src/smt/tactic/smt_tactic_core.cpp:52:5
    #6 0x555d3325a126 in mk_seq_smt_tactic(ast_manager&, params_ref const&) /yuhao/z3/build/../src/smt/tactic/smt_tactic_core.cpp:409:12
    #7 0x555d3325a126 in mk_smt_tactic_core(ast_manager&, params_ref const&, symbol const&) /yuhao/z3/build/../src/smt/tactic/smt_tactic_core.cpp:419:78
    #8 0x555d3227dfd1 in mk_smt_tactic(ast_manager&, params_ref const&) /yuhao/z3/build/../src/tactic/smtlogics/smt_tactic.cpp:30:12
    #9 0x555d32283229 in mk_qfbv_tactic(ast_manager&, params_ref const&) /yuhao/z3/build/../src/tactic/smtlogics/qfbv_tactic.cpp:126:61
    #10 0x555d3226b688 in smt_strategic_solver_factory::operator()(ast_manager&, params_ref const&, bool, bool, bool, symbol const&) /yuhao/z3/build/../src/tactic/portfolio/smt_strategic_solver.cpp:181:17
    #11 0x555d35318dee in cmd_context::mk_solver() /yuhao/z3/build/../src/cmd_context/cmd_context.cpp:2244:16
    #12 0x555d35320039 in cmd_context::init_manager_core(bool) /yuhao/z3/build/../src/cmd_context/cmd_context.cpp:862:9
    #13 0x555d3523e93f in cmd_context::m() const /yuhao/z3/build/../src/cmd_context/cmd_context.h:412:63
    #14 0x555d3523e93f in smt2::parser::m() const /yuhao/z3/build/../src/parsers/smt2/smt2parser.cpp:123:48
    #15 0x555d3523e93f in smt2::parser::expr_stack() /yuhao/z3/build/../src/parsers/smt2/smt2parser.cpp:242:32
    #16 0x555d3523e93f in smt2::parser::parse_check_sat() /yuhao/z3/build/../src/parsers/smt2/smt2parser.cpp:2631:29

SUMMARY: AddressSanitizer: 151532 byte(s) leaked in 533 allocation(s).