heap-use-after-free at src/smt/theory_bv.cpp:1414

[wintered]

[533] % z3 small.smt2
unknown
[534] % z3release small.smt2
unknown
[535] % z3san small.smt2
=================================================================
==30783==ERROR: AddressSanitizer: heap-use-after-free on address 0x61c00003d27c at pc 0x563cdfbc1164 bp 0x7f2497f8cf90 sp 0x7f2497f8cf80
READ of size 1 at 0x61c00003d27c thread T3
  #0 0x563cdfbc1163 in smt::theory_bv::relevant_eh(app*) ../src/smt/theory_bv.cpp:1414
  #1 0x563cdeec9f4f in smt::context::relevant_eh(expr*) ../src/smt/smt_context.cpp:1576
  #2 0x563cdef4f28b in smt::relevancy_propagator_imp::set_relevant(expr*) ../src/smt/smt_relevancy.cpp:308
  #3 0x563cdef4f28b in smt::relevancy_propagator_imp::mark_as_relevant(expr*) ../src/smt/smt_relevancy.cpp:336
  #4 0x563cdef4f28b in smt::relevancy_propagator_imp::propagate_relevant_app(app*) ../src/smt/smt_relevancy.cpp:357
  #5 0x563cdef4f28b in smt::relevancy_propagator_imp::propagate() ../src/smt/smt_relevancy.cpp:485
  #6 0x563cdeeb2c2e in smt::context::propagate_relevancy(unsigned int) ../src/smt/smt_context.cpp:1599
  #7 0x563cdeeeb7d3 in smt::context::propagate() ../src/smt/smt_context.cpp:1676
  #8 0x563cdf8ca414 in smt::lookahead::choose() ../src/smt/smt_lookahead.cpp:107
  #9 0x563cdf5b0d46 in smt::kernel::imp::next_cube() ../src/smt/smt_kernel.cpp:193
  #10 0x563cdf5b0d46 in smt::kernel::next_cube() ../src/smt/smt_kernel.cpp:367
  #11 0x563cdf671bea in cube ../src/smt/smt_solver.cpp:45
  #12 0x563cdf671bea in cube ../src/smt/smt_solver.cpp:288
  #13 0x563ce0606afa in parallel_tactic::cube_and_conquer(parallel_tactic::solver_state&) ../src/solver/parallel_tactic.cpp:501
  #14 0x563ce060de45 in parallel_tactic::run_solver() ../src/solver/parallel_tactic.cpp:634
  #15 0x563ce0610b10 in parallel_tactic::solve(ref<model>&)::{lambda()#1}::operator()() const ../src/solver/parallel_tactic.cpp:670
  #16 0x563ce0610b10 in void std::__invoke_impl<void, parallel_tactic::solve(ref<model>&)::{lambda()#1}>(std::__invoke_other, parallel_tactic::solve(ref<model>&)::{lambda()#1}&&) /usr/include/c++/7/bits/invoke.h:60
  #17 0x563ce0610b10 in std::__invoke_result<parallel_tactic::solve(ref<model>&)::{lambda()#1}>::type std::__invoke<parallel_tactic::solve(ref<model>&)::{lambda()#1}>(std::__invoke_result&&, (parallel_tactic::solve(ref<model>&)::{lambda()#1}&&)...) /usr/include/c++/7/bits/invoke.h:95
  #18 0x563ce0610b10 in decltype (__invoke((_S_declval<0ul>)())) std::thread::_Invoker<std::tuple<parallel_tactic::solve(ref<model>&)::{lambda()#1}> >::_M_invoke<0ul>(std::_Index_tuple<0ul>) /usr/include/c++/7/thread:234
  #19 0x563ce0610b10 in std::thread::_Invoker<std::tuple<parallel_tactic::solve(ref<model>&)::{lambda()#1}> >::operator()() /usr/include/c++/7/thread:243
  #20 0x563ce0610b10 in std::thread::_State_impl<std::thread::_Invoker<std::tuple<parallel_tactic::solve(ref<model>&)::{lambda()#1}> > >::_M_run() /usr/include/c++/7/thread:186
  #21 0x7f249c3626de (/usr/lib/x86_64-linux-gnu/libstdc++.so.6+0xbd6de)
  #22 0x7f249c6356da in start_thread (/lib/x86_64-linux-gnu/libpthread.so.0+0x76da)
  #23 0x7f249ba1f88e in __clone (/lib/x86_64-linux-gnu/libc.so.6+0x12188e)
...
SUMMARY: AddressSanitizer: heap-use-after-free ../src/smt/theory_bv.cpp:1414 in smt::theory_bv::relevant_eh(app*)
...
==30783==ABORTING
[536] % 
[536] % cat small.smt2
(set-option :rewriter.flat false)
(set-option :smt.phase_selection 5)
(set-option :parallel.enable true)
(set-option :smt.arith.solver 1)
(set-option :smt.threads 4)
(declare-fun c () (_ BitVec 32))
(declare-fun d (Int Int) Int)
(declare-fun a () (_ BitVec 32))
(declare-fun oh () Bool)
(declare-fun ih () Bool)
(declare-fun of () Bool)
(declare-fun if () Bool)
(declare-fun aa () (_ BitVec 32))
(declare-fun k () (_ BitVec 32))
(declare-fun ka () (_ BitVec 32))
(declare-fun b () (_ BitVec 32))
(declare-fun ba () (_ BitVec 32))
(declare-fun l () (_ BitVec 32))
(declare-fun la () (_ BitVec 32))
(declare-fun mh () (_ BitVec 32))
(declare-fun jh () (_ BitVec 32))
(declare-fun ac () Bool)
(declare-fun jf () (_ BitVec 32))
(declare-fun ad () Bool)
(assert (not (= (not ih) (bvslt l c) (bvslt la c) (= (= b ba) (or
(distinct a aa) (distinct k ka) (distinct l la))) (= (d 0 7) 7) (=>
(not oh) (= jh #x00000000)) (or ac (=> (= (d 0 7) 0) (= (not ih) (= mh
#x00000000)) (= mh #x00000000)) (=> (=> of (= jf #x00000005) ad (= (=
(d 0 4117) 0) (not if))) (=> (not if) (= (d 0 4117) 0) (not of) (= jf
#x00000000)))))))
(check-sat-using (then qfnra qfaufbv))
[537] %

OS: Ubuntu 18.04
Commit: 626d018