(smt.threads=3, rewriter.flat=false, smt.ematching=false) Segmentation fault

[muchang]

Hi,
For this case, Z3 throws out a segmentation fault:

[626] % z3 small.smt2
unsat
[627] % z3 smt.threads=3 rewriter.flat=false smt.ematching=false small.smt2
Segmentation fault
[628] % z3release smt.threads=3 rewriter.flat=false smt.ematching=false small.smt2
Segmentation fault
[629] % z3san smt.threads=3 rewriter.flat=false smt.ematching=false small.smt2
=================================================================
==24360==ERROR: AddressSanitizer: heap-use-after-free on address 0x60700003e328 at pc 0x55b91c7f6eae bp 0x7f6c4affde00 sp 0x7f6c4affddf0
READ of size 8 at 0x60700003e328 thread T1
  #0 0x55b91c7f6ead in smt::theory_array::merge_eh(int, int, int, int) ../src/smt/theory_array.cpp:60
  #1 0x55b91c918fa0 in smt::theory_array_full::merge_eh(int, int, int, int) ../src/smt/theory_array_full.cpp:331
  #2 0x55b91c7ec56a in union_find<smt::theory_array>::merge(unsigned int, unsigned int) ../src/util/union_find.h:129
  #3 0x55b91c7ec56a in smt::theory_array::new_eq_eh(int, int) ../src/smt/theory_array.cpp:305
  #4 0x55b91bc57ca4 in smt::context::propagate_th_eqs() ../src/smt/smt_context.cpp:1616
  #5 0x55b91bc57ca4 in smt::context::propagate() ../src/smt/smt_context.cpp:1683
  #6 0x55b91bc63b67 in smt::context::bounded_search() ../src/smt/smt_context.cpp:3719
  #7 0x55b91bc647c7 in smt::context::search() ../src/smt/smt_context.cpp:3603
  #8 0x55b91bc66819 in smt::context::check(unsigned int, expr* const*, bool) ../src/smt/smt_context.cpp:3486
  #9 0x55b91c2d5b35 in operator() ../src/smt/smt_parallel.cpp:140
  #10 0x55b91c2d5b35 in operator() ../src/smt/smt_parallel.cpp:191
  #11 0x55b91c2d5b35 in __invoke_impl<void, smt::parallel::operator()(const expr_ref_vector&)::<lambda()> > /usr/include/c++/7/bits/invoke.h:60
  #12 0x55b91c2d5b35 in __invoke<smt::parallel::operator()(const expr_ref_vector&)::<lambda()> > /usr/include/c++/7/bits/invoke.h:95
  #13 0x55b91c2d5b35 in _M_invoke<0> /usr/include/c++/7/thread:234
  #14 0x55b91c2d5b35 in operator() /usr/include/c++/7/thread:243
  #15 0x55b91c2d5b35 in _M_run /usr/include/c++/7/thread:186
  #16 0x7f6c4ebaf6de (/usr/lib/x86_64-linux-gnu/libstdc++.so.6+0xbd6de)
  #17 0x7f6c4ee826da in start_thread (/lib/x86_64-linux-gnu/libpthread.so.0+0x76da)
  #18 0x7f6c4e26c88e in __clone (/lib/x86_64-linux-gnu/libc.so.6+0x12188e)
...
SUMMARY: AddressSanitizer: heap-use-after-free ../src/smt/theory_array.cpp:60 in smt::theory_array::merge_eh(int, int, int, int)
...
==24360==ABORTING
[630] % 
[630] % cat small.smt2
(declare-sort Loc 0)
(define-sort a () (Set Loc))
(declare-sort FldLoc 0)
(declare-fun msz () Loc)
(declare-fun b (FldLoc Loc) Loc)
(declare-fun c (FldLoc Loc Loc) FldLoc)
(declare-fun d (FldLoc a Loc) Loc)
(declare-fun bsz (FldLoc Loc Loc Loc) Bool)
(declare-fun e (a a FldLoc FldLoc) Bool)
(declare-fun asz () a)
(declare-fun g () a)
(declare-fun h () a)
(declare-fun i () a)
(declare-fun sz () a)
(declare-fun j () Loc)
(declare-fun k () Loc)
(declare-fun l (FldLoc Loc Loc) a)
(declare-fun m (a FldLoc Loc Loc) Bool)
(declare-fun lstsz () Loc)
(declare-fun n () Loc)
(declare-fun aa () FldLoc)
(declare-fun nextu1sz () FldLoc)
(declare-fun o () Bool)
(declare-fun p () a)
(declare-fun q () a)
(declare-fun r () a)
(declare-fun s () a)
(declare-fun ab () a)
(declare-fun t () a)
(declare-fun w () a)
(declare-fun tmpu2sz () Loc)
(assert (forall ((y Loc)) (bsz aa msz (b aa msz) y)))
(assert (forall ((y Loc)) (bsz aa tmpu2sz (b aa tmpu2sz) y)))
(assert (forall ((y Loc)) (bsz aa k (b aa k) y)))
(assert (forall ((y Loc)) (or (not (bsz aa msz y y)) (= msz y))))
(assert (forall ((y Loc)) (= tmpu2sz y)))
(assert (forall ((y Loc)) (or (not (= (b aa k) y)) (= k y))))
(assert (bsz aa msz (b aa msz) (b aa msz)))
(assert (bsz aa tmpu2sz (b aa tmpu2sz) (b aa tmpu2sz)))
(assert (bsz aa k (b aa k) (b aa k)))
(assert (forall ((f FldLoc)) (bsz f msz (d f s msz) (d f s msz))))
(assert (forall ((f FldLoc)) (bsz f n (d f s n) (d f s n))))
(assert (forall ((f FldLoc)) (bsz f k (d f s k) (d f s k))))
(assert (forall ((f FldLoc)) (bsz f tmpu2sz (d f s tmpu2sz) (d f s tmpu2sz))))
(assert (= (b (c aa k (b aa tmpu2sz)) k) (b aa tmpu2sz)))
(assert (or (= tmpu2sz k) (= (b aa tmpu2sz) (b (c aa k (b aa tmpu2sz)) tmpu2sz))))
(assert (= (b aa msz) msz (b nextu1sz msz)))
(assert (= sz (union g sz)))
(assert (= w g))
(assert (m t aa lstsz j))
(assert (= ab (l aa j msz) s (union ab t)))
(assert (m q aa k msz))
(assert (= r (union q p)))
(assert (= q (l aa k msz)))
(assert (= asz (union sz asz)))
(assert (e h asz aa aa))
(assert (= j lstsz))
(assert (= i (union (setminus g h) (union (intersection asz h) (setminus asz asz)))))
(assert (bsz aa lstsz j j))
(assert (bsz aa k msz msz))
(assert (or (= (b aa k) msz) (not o)))
(assert (not (= tmpu2sz msz)))
(assert (= w (l aa lstsz msz)))
(assert (not (= j msz)))
(assert (m ab aa j msz))
(assert (= t (l aa lstsz j)))
(assert (= s h))
(assert (not (= k msz)))
(assert (m p aa n k))
(assert (= r (union (intersection asz h) (setminus asz asz))))
(assert (= p (l aa n k)))
(assert (= asz (union i asz)))
(assert (distinct tmpu2sz (b aa k)))
(assert (= n lstsz))
(assert (bsz aa n k k))
(assert (bsz aa j msz msz))
(assert (forall ((u Loc) (v Loc) (z Loc))
     (and (or (bsz (c aa k (b aa tmpu2sz)) z u v))
     (or (bsz aa z v v) (bsz aa z u k)
      (and (= k v) (not (bsz aa (b aa tmpu2sz) k k)))
      (not (bsz (c aa k (b aa tmpu2sz)) z u v))))))
(assert (forall ((x Loc)) (bsz aa x x x)))
(assert (forall ((x Loc) (y Loc)) (or (not (bsz aa x y x)) (= x y))))
(assert (forall ((x Loc) (y Loc) (z Loc)) (bsz aa x z y)))
(assert (forall ((x Loc) (y Loc) (z Loc)) (bsz aa x y z)))
(assert (forall ((x Loc) (z Loc)) (bsz aa x z z)))
(assert (forall ((u Loc) (x Loc) (y Loc)) (bsz aa x y u)))
(assert (forall ((u Loc) (x Loc) (z Loc)) (bsz aa x u z)))
(check-sat)
[631] %

OS: Ubuntu 18.04
Commit: 785c9a1