heap-use-after-free ../src/smt/theory_array.cpp:369

[wintered]

[560] % z3san small.smt2
=================================================================
==1426==ERROR: AddressSanitizer: heap-use-after-free on address 0x61c000039267 at pc 0x55959a15d811 bp 0x7f5e34f83430 sp 0x7f5e34f83420
READ of size 1 at 0x61c000039267 thread T34
==1426==AddressSanitizer: while reporting a bug found another one. Ignoring.
  #0 0x55959a15d810 in smt::theory_array::final_check_eh() ../src/smt/theory_array.cpp:369
  #1 0x5595995c7704 in smt::context::final_check() ../src/smt/smt_context.cpp:3860
  #2 0x5595995d7ec6 in smt::context::bounded_search() ../src/smt/smt_context.cpp:3776
  #3 0x5595995d87c7 in smt::context::search() ../src/smt/smt_context.cpp:3603
  #4 0x5595995da819 in smt::context::check(unsigned int, expr* const*, bool) ../src/smt/smt_context.cpp:3486
  #5 0x559599c49b35 in operator() ../src/smt/smt_parallel.cpp:140
  #6 0x559599c49b35 in operator() ../src/smt/smt_parallel.cpp:191
  #7 0x559599c49b35 in __invoke_impl<void, smt::parallel::operator()(const expr_ref_vector&)::<lambda()> > /usr/include/c++/7/bits/invoke.h:60
  #8 0x559599c49b35 in __invoke<smt::parallel::operator()(const expr_ref_vector&)::<lambda()> > /usr/include/c++/7/bits/invoke.h:95
  #9 0x559599c49b35 in _M_invoke<0> /usr/include/c++/7/thread:234
  #10 0x559599c49b35 in operator() /usr/include/c++/7/thread:243
  #11 0x559599c49b35 in _M_run /usr/include/c++/7/thread:186
  #12 0x7f5e476036de (/usr/lib/x86_64-linux-gnu/libstdc++.so.6+0xbd6de)
  #13 0x7f5e478d66da in start_thread (/lib/x86_64-linux-gnu/libpthread.so.0+0x76da)
  #14 0x7f5e46cc088e in __clone (/lib/x86_64-linux-gnu/libc.so.6+0x12188e)
...
SUMMARY: AddressSanitizer: heap-use-after-free ../src/smt/theory_array.cpp:369 in smt::theory_array::final_check_eh()
...
==1426==ABORTING
[561] % 
[561] % cat small.smt2
(set-option :smt.phase_selection 5)
(set-option :parallel.enable true)
(set-option :smt.arith.solver 1)
(set-option :smt.threads 2)
(declare-fun a () (_ BitVec 32))
(declare-fun b (Int) Int)
(declare-fun c () Bool)
(declare-fun d () (_ BitVec 32))
(declare-fun l () Bool)
(declare-fun e () (_ BitVec 32))
(declare-fun m () (_ BitVec 32))
(declare-fun f () (_ BitVec 32))
(declare-fun n () (_ BitVec 32))
(declare-fun j () Bool)
(define-fun k () Bool (=> (= (b 0) 8) (and (bvsge f a) (bvslt n a) (= (= m f n) (= c l)) (=> l (= d e) c)) j))
(assert (not k))
(check-sat)
[562] %

OS: Ubuntu 18.04
Commit: 785c9a1