Potential issue in arithmetic optimization

[merlinsun]

Hi,

I came across a potential correctness issue in the arithmetic optimization when using opt.optsmt_engine=symba. The two following inputs, which appear semantically similar, yield different objective values:

$ z3 opt.optsmt_engine=symba small_int.smt2        
sat
(objectives
 ((- a) oo)
 (a oo)
)
$ cat small_int.smt2
(set-option :opt.priority box)
(declare-const a Int) 
(assert (< 0 (div a 0))) 
(maximize (- a)) 
(maximize a) 
(check-sat) 
(get-objectives) 
$ z3 opt.optsmt_engine=symba small_mix.smt2  
sat
(objectives
 ((- a) 0)
 (a 0)
)
$ cat small_mix.smt2
(set-option :opt.priority box)
(declare-const a Real) 
(assert (< 0 (div (to_int a) 0))) 
(maximize (- a)) 
(maximize a) 
(check-sat) 
(get-objectives)            

Commit: https://github.com/Z3Prover/z3/commit/423930dbadb68540ee18681e76f249b0774fedcc

---

[NikolajBjorner]

thanks

[merlinsun]

Glad it helped!

[qobilidop]

We ran into a similar ASAN memory leak issue when we tried to import the latest Z3 to Google.

CC @smolkaj @kheradmandG @jonathan-dilorenzo

[NikolajBjorner]

extra brownie points for listing the full stack

[merlinsun]

@NikolajBjorner Thank you for the response. The full stack trace is quite long, so I’ve attached it here for your convenience. The Z3 commit in use is: https://github.com/Z3Prover/z3/commit/423930dbadb68540ee18681e76f249b0774fedcc.

stack.txt

[qobilidop]

Add one more stack trace from our side:

Indirect leak of 24 byte(s) in 1 object(s) allocated from:
    #0 0x56094a1cf29d in operator new(unsigned long) third_party/llvm/llvm-project/compiler-rt/lib/asan/asan_new_delete.cpp:86:3
    #1 0x7feb61f8348b in __libcpp_operator_new<unsigned long> third_party/crosstool/v18/stable/src/libcxx/include/__new/allocate.h:37:10
    #2 0x7feb61f8348b in __libcpp_allocate<std::__u::__hash_node<std::__u::__hash_value_type<unsigned int, unsigned int>, void *> > third_party/crosstool/v18/stable/src/libcxx/include/__new/allocate.h:64:28
    #3 0x7feb61f8348b in allocate third_party/crosstool/v18/stable/src/libcxx/include/__memory/allocator.h:106:14
    #4 0x7feb61f8348b in allocate third_party/crosstool/v18/stable/src/libcxx/include/__memory/allocator_traits.h:259:16
    #5 0x7feb61f8348b in __construct_node_hash<const std::__u::piecewise_construct_t &, std::__u::tuple<const unsigned int &>, std::__u::tuple<> > third_party/crosstool/v18/stable/src/libcxx/include/__hash_table:1842:21
    #6 0x7feb61f8348b in std::__u::pair<std::__u::__hash_iterator<std::__u::__hash_node<std::__u::__hash_value_type<unsigned int, unsigned int>, void*>*>, bool> std::__u::__hash_table<std::__u::__hash_value_type<unsigned int, unsigned int>, std::__u::__unordered_map_hasher<unsigned int, std::__u::__hash_value_type<unsigned int, unsigned int>, std::__u::hash<unsigned int>, std::__u::equal_to<unsigned int>, true>, std::__u::__unordered_map_equal<unsigned int, std::__u::__hash_value_type<unsigned int, unsigned int>, std::__u::equal_to<unsigned int>, std::__u::hash<unsigned int>, true>, std::__u::allocator<std::__u::__hash_value_type<unsigned int, unsigned int>>>::__emplace_unique_key_args<unsigned int, std::__u::piecewise_construct_t const&, std::__u::tuple<unsigned int const&>, std::__u::tuple<>>(unsigned int const&, std::__u::piecewise_construct_t const&, std::__u::tuple<unsigned int const&>&&, std::__u::tuple<>&&) third_party/crosstool/v18/stable/src/libcxx/include/__hash_table:1549:25
    #7 0x7feb282e5110 in operator[] third_party/crosstool/v18/stable/src/libcxx/include/unordered_map:1743:8
    #8 0x7feb282e5110 in lp::var_register::add_var(unsigned int, bool) third_party/z3/src/math/lp/var_register.h:65:13
    #9 0x7feb283686e6 in register_new_external_var third_party/z3/src/math/lp/lar_solver.cpp:1927:31
    #10 0x7feb283686e6 in add_non_basic_var_to_core_fields third_party/z3/src/math/lp/lar_solver.cpp:1935:9
    #11 0x7feb283686e6 in lp::lar_solver::add_var(unsigned int, bool) third_party/z3/src/math/lp/lar_solver.cpp:1916:9
    #12 0x7feb294a7979 in smt::theory_lra::imp::add_const(int, unsigned int&, bool) third_party/z3/src/smt/theory_lra.cpp:241:20
    #13 0x7feb294978da in get_one third_party/z3/src/smt/theory_lra.cpp:250:16
    #14 0x7feb294978da in smt::theory_lra::imp::init() third_party/z3/src/smt/theory_lra.cpp:861:9
    #15 0x7feb29497811 in smt::theory_lra::init() third_party/z3/src/smt/theory_lra.cpp:4214:12
    #16 0x7feb290e1444 in smt::context::register_plugin(smt::theory*) third_party/z3/src/smt/smt_context.cpp:2900:13
    #17 0x7feb291a760d in smt::setup::setup_lra_arith() third_party/z3/src/smt/smt_setup.cpp
    #18 0x7feb291a86ce in smt::setup::setup_arith() third_party/z3/src/smt/smt_setup.cpp:687:13
    #19 0x7feb291a2886 in smt::setup::setup_unknown() third_party/z3/src/smt/smt_setup.cpp:819:9
    #20 0x7feb291a408b in smt::setup::setup_QF_S() third_party/z3/src/smt/smt_setup.cpp
    #21 0x7feb291a30a8 in smt::setup::setup_default() third_party/z3/src/smt/smt_setup.cpp:135:13
    #22 0x7feb291a2682 in smt::setup::operator()(smt::config_mode) third_party/z3/src/smt/smt_setup.cpp:68:25
    #23 0x7feb290fc5bb in smt::context::setup_context(bool) third_party/z3/src/smt/smt_context.cpp:3659:9
    #24 0x7feb290f669d in smt::context::push() third_party/z3/src/smt/smt_context.cpp:3013:9
    #25 0x7feb29146c3c in smt::kernel::push() third_party/z3/src/smt/smt_kernel.cpp:101:25
    #26 0x7feb291adabf in (anonymous namespace)::smt_solver::push_core() third_party/z3/src/smt/smt_solver.cpp:177:23
    #27 0x7feb296bd7c4 in solver_na2as::push() third_party/z3/src/solver/solver_na2as.cpp:86:5
    #28 0x7feb29697e9b in combined_solver::push() third_party/z3/src/solver/combined_solver.cpp:179:20
    #29 0x7feb2792e272 in Z3_solver_push third_party/z3/src/api/api_solver.cpp:481:27
    #30 0x7feb60bed2cd in push third_party/z3/src/api/c++/z3++.h:2803:23

Some notes:

• This ASAN memory leak issue is triggered with some Google internal test code.
• The stack trace is truncated at where the Google internal code calls Z3 for confidentiality requirements.
• The Z3 commit in use is https://github.com/Z3Prover/z3/commit/b2f01706beb190c233439a4aceb110fe9e6a7cfc.
• I suspected this is the same issue as what's reported above because there are some similarities in the stack trace.

[NikolajBjorner]

I was compiling z3 yesterday with ASAN settings on ubuntu to repro this, but either the repro is gone or my settings are wrong.

CFLAGS='-fsanitize=address ASAN_OPTIONS=detect_leaks=1' python3 scripts/mk_make.py -b build

[merlinsun]

Thanks for looking into this!

I was able to trigger the memory leak on https://github.com/Z3Prover/z3/commit/a3c8bbb461b80bc6d35499b8224585aa330ed678 using the following configuration:

CFLAGS+="-fsanitize=address -fsanitize-recover=address -U_FORTIFY_SOURCE -fno-omit-frame-pointer -fno-common" LDFLAGS+="-fsanitize=address" python3 scripts/mk_make.py -d

I also tried the settings you used, and I can confirm that the issue does not reproduce with those.

Hope this helps!

[NikolajBjorner]

copilot sorted it out

[merlinsun]

Cool!

[snova-nathanz]

Just checking

copilot sorted it out

Does this mean that this issue is fixed in its entirety, or just the memory leak?

[merlinsun]

Hi, @snova-nathanz

I believe Nikolaj was referring specifically to the memory leak fix. The inconsistency issue still appears to be unresolved.