(smt.phase_selection=5, parallel.enable, smt.threads=5, rewriter.cache_all) Heap-use-after-free at ../src/smt/theory_datatype.cpp:490

[muchang]

Hi,
For this case, Z3 ASAN build throws out a heap-use-after-free:

[631] % z3 small.smt2
unknown
[632] % z3release small.smt2
unknown
[633] % z3san small.smt2
=================================================================
==5628==ERROR: AddressSanitizer: heap-use-after-free on address 0x61c00003d2c0 at pc 0x55feb9c59d28 bp 0x7f5e0b57d650 sp 0x7f5e0b57d640
READ of size 4 at 0x61c00003d2c0 thread T3
  #0 0x55feb9c59d27 in smt::theory_datatype::final_check_eh() ../src/smt/theory_datatype.cpp:490
  #1 0x55feb9110e14 in smt::context::final_check() ../src/smt/smt_context.cpp:3860
  #2 0x55feb9120c26 in smt::context::bounded_search() ../src/smt/smt_context.cpp:3776
  #3 0x55feb9121527 in smt::context::search() ../src/smt/smt_context.cpp:3603
  #4 0x55feb91235b9 in smt::context::check(unsigned int, expr* const*, bool) ../src/smt/smt_context.cpp:3486
  #5 0x55feb979da44 in smt::parallel::operator()(ref_vector<expr, ast_manager> const&) ../src/smt/smt_parallel.cpp:39
  #6 0x55feb912393e in smt::context::check(unsigned int, expr* const*, bool) ../src/smt/smt_context.cpp:3475
  #7 0x55feba89b137 in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67
  #8 0x55feba839a51 in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:330
  #9 0x55feba826a42 in solver::check_sat(ref_vector<expr, ast_manager> const&) ../src/solver/solver.h:149
  #10 0x55feba826a42 in parallel_tactic::solver_state::simplify() ../src/solver/parallel_tactic.cpp:265
  #11 0x55feba826a42 in parallel_tactic::cube_and_conquer(parallel_tactic::solver_state&) ../src/solver/parallel_tactic.cpp:481
  #12 0x55feba82f015 in parallel_tactic::run_solver() ../src/solver/parallel_tactic.cpp:634
  #13 0x55feba831ce0 in parallel_tactic::solve(ref<model>&)::{lambda()#1}::operator()() const ../src/solver/parallel_tactic.cpp:670
  #14 0x55feba831ce0 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
  #15 0x55feba831ce0 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
  #16 0x55feba831ce0 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
  #17 0x55feba831ce0 in std::thread::_Invoker<std::tuple<parallel_tactic::solve(ref<model>&)::{lambda()#1}> >::operator()() /usr/include/c++/7/thread:243
  #18 0x55feba831ce0 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
  #19 0x7f5e100c46de (/usr/lib/x86_64-linux-gnu/libstdc++.so.6+0xbd6de)
  #20 0x7f5e103976da in start_thread (/lib/x86_64-linux-gnu/libpthread.so.0+0x76da)
  #21 0x7f5e0f78188e in __clone (/lib/x86_64-linux-gnu/libc.so.6+0x12188e)
...
SUMMARY: AddressSanitizer: heap-use-after-free ../src/smt/theory_datatype.cpp:490 in smt::theory_datatype::final_check_eh()
...
==5628==ABORTING
[634] % 
[634] % cat small.smt2
(set-option :smt.phase_selection 5)
(set-option :parallel.enable true)
(set-option :smt.threads 5)
(set-option :rewriter.cache_all true)
(declare-sort T)
(declare-datatypes ((L 0)) (((C (h T) (t L)) N)))
(declare-datatypes ((O 0)) (((M) (S (u T)))))
(declare-fun a () Bool)
(declare-fun b () O)
(declare-fun c () Bool)
(declare-fun d ((Array T Bool) L) Bool)
(declare-fun e ((Array T Bool) L) O)
(declare-fun f ((Array T Bool) L) Bool)
(declare-fun g () Bool)
(declare-fun h ((Array T Bool) L) Bool)
(declare-fun i () Bool)
(assert (forall ((j (Array T Bool)) (k L)) (= (d j k) (ite ((_ is S) (e j k)) (f j k) (ite ((_ is M) (e j k)) (and (f j k)) a)))))
(assert (forall ((l (Array T Bool)) (m L)) (distinct (e l m) (ite ((_ is C) m) (ite (l (h m)) (S (h m)) (e l (t m))) (ite ((_ is N) m) M b)))))
(assert (forall ((n (Array T Bool)) (o L)) (distinct (f n o) (ite ((_ is C) o) (or (or (n (h o)))) c))))
(assert (forall ((p (Array T Bool)) (q L)) (= (h p q) (ite ((_ is C) q) (and (xor (d p q) (d p q))) (ite ((_ is N) q) (d p q) g)))))
(assert (forall ((q L) (p (Array T Bool))) (ite (and (h p (t q)) (d p q)) ((_ is C) q) (ite ((_ is N) q) (d p q) i))))
(check-sat-using qflia)
[635] %

OS: Ubuntu 18.04
Commit: 9f6a733