(rewriter.flat, smt.phase_selection, smt.threads, model_validate) Non-deterministic memory leak

[rainoftime]

Hi, for the following formula, z3 1591609

(declare-const x Bool)
(set-option :rewriter.flat false)
(set-option :smt.phase_selection 1)
(set-option :smt.threads 2)
(declare-fun sk () Real)
(assert (exists ((k Real)) (exists ((s Real)) (let (($x40 (= sk 0.0))) (and x (> s 2.0) (= s (* k k k)) (= s (+ 1.0 (* sk sk))))))))
(check-sat-using ctx-solver-simplify)

z3 model_validate=true xx.smt2

....
ast_manager LEAKED: 39

=================================================================
==631773==ERROR: LeakSanitizer: detected memory leaks

Direct leak of 456 byte(s) in 19 object(s) allocated from:
    #0 0x7f86579dc279 in __interceptor_malloc /build/gcc/src/gcc/libsanitizer/asan/asan_malloc_linux.cpp:145
    #1 0x55e1d73c50df in memory::allocate(unsigned long) ../src/util/memory_manager.cpp:273
    #2 0x55e1d73c4bc0 in memory::allocate(char const*, int, char const*, unsigned long) ../src/util/memory_manager.cpp:212
    #3 0x55e1d55672ab in smt::theory_lra::imp::mk_value(smt::enode*, smt::model_generator&) (/home/peisen/test/tofuzz/z3-debug/build/z3+0x15f72ab)
    #4 0x55e1d552ae47 in smt::theory_lra::mk_value(smt::enode*, smt::model_generator&) ../src/smt/theory_lra.cpp:3838
    #5 0x55e1d51c8db0 in smt::model_generator::mk_value_procs(obj_map<smt::enode, smt::model_value_proc*>&, ptr_vector<smt::enode>&, ptr_vector<smt::model_value_proc>&) ../src/smt/smt_model_generator.cpp:115
    #6 0x55e1d51cbf59 in smt::model_generator::mk_values() ../src/smt/smt_model_generator.cpp:299
    #7 0x55e1d51cff50 in smt::model_generator::mk_model() ../src/smt/smt_model_generator.cpp:502
    #8 0x55e1d52aa95b in smt::context::mk_proto_model() ../src/smt/smt_context.cpp:4515
    #9 0x55e1d52ab242 in smt::context::get_model(ref<model>&) ../src/smt/smt_context.cpp:4550
    #10 0x55e1d529cbc2 in smt::context::check_finalize(lbool) ../src/smt/smt_context.cpp:3397
    #11 0x55e1d529e273 in smt::context::check(unsigned int, expr* const*, bool) ../src/smt/smt_context.cpp:3565
    #12 0x55e1d57acb16 in operator() ../src/smt/smt_parallel.cpp:159
    #13 0x55e1d57addfa in operator() ../src/smt/smt_parallel.cpp:223
    #14 0x55e1d57b1127 in __invoke_impl<void, smt::parallel::operator()(const expr_ref_vector&)::<lambda()> > /usr/include/c++/11.1.0/bits/invoke.h:61
    #15 0x55e1d57b10dc in __invoke<smt::parallel::operator()(const expr_ref_vector&)::<lambda()> > /usr/include/c++/11.1.0/bits/invoke.h:96
    #16 0x55e1d57b1089 in _M_invoke<0> /usr/include/c++/11.1.0/bits/std_thread.h:253
    #17 0x55e1d57b105d in operator() /usr/include/c++/11.1.0/bits/std_thread.h:260
    #18 0x55e1d57b1041 in _M_run /usr/include/c++/11.1.0/bits/std_thread.h:211
    #19 0x7f86577c13c3 in execute_native_thread_routine /build/gcc/src/gcc/libstdc++-v3/src/c++11/thread.cc:82

Direct leak of 432 byte(s) in 18 object(s) allocated from:
    #0 0x7f86579dc279 in __interceptor_malloc /build/gcc/src/gcc/libsanitizer/asan/asan_malloc_linux.cpp:145
    #1 0x55e1d73c50df in memory::allocate(unsigned long) ../src/util/memory_manager.cpp:273
    #2 0x55e1d73c4bc0 in memory::allocate(char const*, int, char const*, unsigned long) ../src/util/memory_manager.cpp:212
    #3 0x55e1d51c8b96 in smt::model_generator::mk_value_procs(obj_map<smt::enode, smt::model_value_proc*>&, ptr_vector<smt::enode>&, ptr_vector<smt::model_value_proc>&) ../src/smt/smt_model_generator.cpp:109
    #4 0x55e1d51cbf59 in smt::model_generator::mk_values() ../src/smt/smt_model_generator.cpp:299
    #5 0x55e1d51cff50 in smt::model_generator::mk_model() ../src/smt/smt_model_generator.cpp:502
    #6 0x55e1d52aa95b in smt::context::mk_proto_model() ../src/smt/smt_context.cpp:4515
    #7 0x55e1d52ab242 in smt::context::get_model(ref<model>&) ../src/smt/smt_context.cpp:4550
    #8 0x55e1d529cbc2 in smt::context::check_finalize(lbool) ../src/smt/smt_context.cpp:3397
    #9 0x55e1d529e273 in smt::context::check(unsigned int, expr* const*, bool) ../src/smt/smt_context.cpp:3565
    #10 0x55e1d57acb16 in operator() ../src/smt/smt_parallel.cpp:159
    #11 0x55e1d57addfa in operator() ../src/smt/smt_parallel.cpp:223