heap-use-after-free on String formula at smt/theory_seq.h:171 (smt.random_seed 5, smt.threads 4, smt.arith.solver 5)

[rainoftime]

Hi, for the following formula,
uaf.txt

z3 (commit 04fec3f) throws a uaf

==153691==ERROR: AddressSanitizer: heap-use-after-free on address 0x61800009cb88 at pc 0x0000014ee1cb bp 0x7f3fd6687220 sp 0x7f3fd6687210
READ of size 8 at 0x61800009cb88 thread T8
    #0 0x14ee1ca in smt::theory_seq::eq::dep() const ../src/smt/theory_seq.h:171
    #1 0x1580ec9 in smt::theory_seq::branch_ternary_variable2(smt::theory_seq::eq const&, bool) ../src/smt/seq_eq_solver.cpp:1044
    #2 0x157cce0 in smt::theory_seq::branch_ternary_variable1() ../src/smt/seq_eq_solver.cpp:754
    #3 0x157861b in smt::theory_seq::branch_variable() ../src/smt/seq_eq_solver.cpp:470
    #4 0x14be65a in smt::theory_seq::final_check_eh() ../src/smt/theory_seq.cpp:411
    #5 0xfc735d in smt::context::final_check() ../src/smt/smt_context.cpp:3857
    #6 0xfc6366 in smt::context::bounded_search() ../src/smt/smt_context.cpp:3773
    #7 0xfc3aa2 in smt::context::search() ../src/smt/smt_context.cpp:3600
    #8 0xfc201b in smt::context::check(unsigned int, expr* const*, bool) ../src/smt/smt_context.cpp:3483
    #9 0x1132e75 in smt::parallel::operator()(ref_vector<expr, ast_manager> const&)::{lambda(int)#3}::operator()(int) const (/home/peisen/test/tofuzz/z3-debug/build/z3+0x1132e75)
    #10 0x1133ac9 in smt::parallel::operator()(ref_vector<expr, ast_manager> const&)::{lambda()#4}::operator()() const (/home/peisen/test/tofuzz/z3-debug/build/z3+0x1133ac9)
    #11 0x1136dbb in _M_invoke<> /usr/include/c++/5/functional:1531
    #12 0x1136ccf in operator() /usr/include/c++/5/functional:1520
    #13 0x1136c5f in _M_run /usr/include/c++/5/thread:115
    #14 0x7f3fdb82ab8d  (/usr/lib/x86_64-linux-gnu/libstdc++.so.6+0xd0b8d)
    #15 0x7f3fdbb446b9 in start_thread (/lib/x86_64-linux-gnu/libpthread.so.0+0x76b9)
    #16 0x7f3fdaf7641c in clone (/lib/x86_64-linux-gnu/libc.so.6+0x10741c)
0x61800009cb88 is located 776 bytes inside of 880-byte region [0x61800009c880,0x61800009cbf0)
freed by thread T8 here:
    #0 0x7f3fdbdf232a in __interceptor_free (/usr/lib/x86_64-linux-gnu/libasan.so.2+0x9832a)
    #1 0x25e3529 in memory::deallocate(void*) ../src/util/memory_manager.cpp:260
    #2 0x1506c6a in vector<smt::theory_seq::eq, true, unsigned int>::expand_vector() ../src/util/vector.h:99
    #3 0x14feec9 in vector<smt::theory_seq::eq, true, unsigned int>::push_back(smt::theory_seq::eq const&) ../src/util/vector.h:419
    #4 0x14f510d in scoped_vector<smt::theory_seq::eq>::push_back(smt::theory_seq::eq const&) ../src/util/scoped_vector.h:121
    #5 0x14e2d45 in smt::theory_seq::new_eq_eh(dependency_manager<scoped_dependency_manager<smt::theory_seq::assumption>::config>::dependency*, smt::enode*, smt::enode*) ../src/smt/theory_seq.cpp:3132
    #6 0x14e0493 in smt::theory_seq::propagate_eq(dependency_manager<scoped_dependency_manager<smt::theory_seq::assumption>::config>::dependency*, svector<smt::literal, unsigned int> const&, expr*, expr*,
 bool) ../src/smt/theory_seq.cpp:2956
    #7 0x14c47da in smt::theory_seq::propagate_eq(dependency_manager<scoped_dependency_manager<smt::theory_seq::assumption>::config>::dependency*, smt::literal, expr*, expr*, bool) ../src/smt/theory_seq.c
pp:857
    #8 0x1580e92 in smt::theory_seq::branch_ternary_variable2(smt::theory_seq::eq const&, bool) ../src/smt/seq_eq_solver.cpp:1043
    #9 0x157cce0 in smt::theory_seq::branch_ternary_variable1() ../src/smt/seq_eq_solver.cpp:754
    #10 0x157861b in smt::theory_seq::branch_variable() ../src/smt/seq_eq_solver.cpp:470
    #11 0x14be65a in smt::theory_seq::final_check_eh() ../src/smt/theory_seq.cpp:411
    #12 0xfc735d in smt::context::final_check() ../src/smt/smt_context.cpp:3857
    #13 0xfc6366 in smt::context::bounded_search() ../src/smt/smt_context.cpp:3773
    #14 0xfc3aa2 in smt::context::search() ../src/smt/smt_context.cpp:3600
    #15 0xfc201b in smt::context::check(unsigned int, expr* const*, bool) ../src/smt/smt_context.cpp:3483
    #16 0x1132e75 in smt::parallel::operator()(ref_vector<expr, ast_manager> const&)::{lambda(int)#3}::operator()(int) const (/home/peisen/test/tofuzz/z3-debug/build/z3+0x1132e75)
    #17 0x1133ac9 in smt::parallel::operator()(ref_vector<expr, ast_manager> const&)::{lambda()#4}::operator()() const (/home/peisen/test/tofuzz/z3-debug/build/z3+0x1133ac9)
    #18 0x1136dbb in _M_invoke<> /usr/include/c++/5/functional:1531
    #19 0x1136ccf in operator() /usr/include/c++/5/functional:1520
    #20 0x1136c5f in _M_run /usr/include/c++/5/thread:115
    #21 0x7f3fdb82ab8d  (/usr/lib/x86_64-linux-gnu/libstdc++.so.6+0xd0b8d)

previously allocated by thread T8 here:
    #0 0x7f3fdbdf2662 in malloc (/usr/lib/x86_64-linux-gnu/libasan.so.2+0x98662)
    #1 0x25e3575 in memory::allocate(unsigned long) ../src/util/memory_manager.cpp:268
    #2 0x1506aa7 in vector<smt::theory_seq::eq, true, unsigned int>::expand_vector() ../src/util/vector.h:90
    #3 0x14feec9 in vector<smt::theory_seq::eq, true, unsigned int>::push_back(smt::theory_seq::eq const&) ../src/util/vector.h:419
    #4 0x158a428 in scoped_vector<smt::theory_seq::eq>::set(unsigned int, smt::theory_seq::eq const&) ../src/util/scoped_vector.h:89
    #5 0x158a1ff in scoped_vector<smt::theory_seq::eq>::erase_and_swap(unsigned int) ../src/util/scoped_vector.h:139
    #6 0x1574a2b in smt::theory_seq::solve_eqs(unsigned int) ../src/smt/seq_eq_solver.cpp:35
    #7 0x14ce213 in smt::theory_seq::simplify_and_solve_eqs() ../src/smt/theory_seq.cpp:1514
    #8 0x14d9658 in smt::theory_seq::propagate() ../src/smt/theory_seq.cpp:2529
    #9 0xfae37f in smt::context::propagate_theories() ../src/smt/smt_context.cpp:1600
    #10 0xfaf114 in smt::context::propagate() ../src/smt/smt_context.cpp:1683
    #11 0xfc5878 in smt::context::bounded_search() ../src/smt/smt_context.cpp:3716
    #12 0xfc3aa2 in smt::context::search() ../src/smt/smt_context.cpp:3600
    #13 0xfc201b in smt::context::check(unsigned int, expr* const*, bool) ../src/smt/smt_context.cpp:3483
    #14 0x1132e75 in smt::parallel::operator()(ref_vector<expr, ast_manager> const&)::{lambda(int)#3}::operator()(int) const (/home/peisen/test/tofuzz/z3-debug/build/z3+0x1132e75)
    #15 0x1133ac9 in smt::parallel::operator()(ref_vector<expr, ast_manager> const&)::{lambda()#4}::operator()() const (/home/peisen/test/tofuzz/z3-debug/build/z3+0x1133ac9)
    #16 0x1136dbb in _M_invoke<> /usr/include/c++/5/functional:1531
    #17 0x1136ccf in operator() /usr/include/c++/5/functional:1520
    #18 0x1136c5f in _M_run /usr/include/c++/5/thread:115
    #21 0x7f3fdb82ab8d  (/usr/lib/x86_64-linux-gnu/libstdc++.so.6+0xd0b8d)

previously allocated by thread T8 here:
    #0 0x7f3fdbdf2662 in malloc (/usr/lib/x86_64-linux-gnu/libasan.so.2+0x98662)
    #1 0x25e3575 in memory::allocate(unsigned long) ../src/util/memory_manager.cpp:268
    #2 0x1506aa7 in vector<smt::theory_seq::eq, true, unsigned int>::expand_vector() ../src/util/vector.h:90
    #3 0x14feec9 in vector<smt::theory_seq::eq, true, unsigned int>::push_back(smt::theory_seq::eq const&) ../src/util/vector.h:419
    #4 0x158a428 in scoped_vector<smt::theory_seq::eq>::set(unsigned int, smt::theory_seq::eq const&) ../src/util/scoped_vector.h:89
    #5 0x158a1ff in scoped_vector<smt::theory_seq::eq>::erase_and_swap(unsigned int) ../src/util/scoped_vector.h:139
    #6 0x1574a2b in smt::theory_seq::solve_eqs(unsigned int) ../src/smt/seq_eq_solver.cpp:35
    #7 0x14ce213 in smt::theory_seq::simplify_and_solve_eqs() ../src/smt/theory_seq.cpp:1514
    #8 0x14d9658 in smt::theory_seq::propagate() ../src/smt/theory_seq.cpp:2529
    #9 0xfae37f in smt::context::propagate_theories() ../src/smt/smt_context.cpp:1600
    #10 0xfaf114 in smt::context::propagate() ../src/smt/smt_context.cpp:1683
    #11 0xfc5878 in smt::context::bounded_search() ../src/smt/smt_context.cpp:3716
    #12 0xfc3aa2 in smt::context::search() ../src/smt/smt_context.cpp:3600
    #13 0xfc201b in smt::context::check(unsigned int, expr* const*, bool) ../src/smt/smt_context.cpp:3483
    #14 0x1132e75 in smt::parallel::operator()(ref_vector<expr, ast_manager> const&)::{lambda(int)#3}::operator()(int) const (/home/peisen/test/tofuzz/z3-debug/build/z3+0x1132e75)
    #15 0x1133ac9 in smt::parallel::operator()(ref_vector<expr, ast_manager> const&)::{lambda()#4}::operator()() const (/home/peisen/test/tofuzz/z3-debug/build/z3+0x1133ac9)
    #16 0x1136dbb in _M_invoke<> /usr/include/c++/5/functional:1531
    #17 0x1136ccf in operator() /usr/include/c++/5/functional:1520
    #18 0x1136c5f in _M_run /usr/include/c++/5/thread:115
    #19 0x7f3fdb82ab8d  (/usr/lib/x86_64-linux-gnu/libstdc++.so.6+0xd0b8d)

Thread T8 created by T0 here:
    #0 0x7f3fdbd901e3 in pthread_create (/usr/lib/x86_64-linux-gnu/libasan.so.2+0x361e3)
    #1 0x7f3fdb82ac93 in std::thread::_M_start_thread(std::shared_ptr<std::thread::_Impl_base>, void (*)()) (/usr/lib/x86_64-linux-gnu/libstdc++.so.6+0xd0c93)

SUMMARY: AddressSanitizer: heap-use-after-free ../src/smt/theory_seq.h:171 smt::theory_seq::eq::dep() const