Heap-use-after-free with a tactic

[merlinsun]

Hi,
For this following instance, z3 996e5b1

$ cat small.smt2
(declare-fun ol_7 () Bool)
(assert (or (not (or false (and ol_7 false false false false) false))))
(check-sat-using dom-simplify)
$ z3asan small.smt2
=================================================================
==210252==ERROR: AddressSanitizer: heap-use-after-free on address 0x606000062aec at pc 0x555c7bfeba01 bp 0x7fff3441a7a0 sp 0x7fff3441a790
READ of size 4 at 0x606000062aec thread T0
    #0 0x555c7bfeba00 in ast::hash() const ../src/ast/ast.h:503
    #1 0x555c7c05fe51 in obj_map<expr, expr*>::key_data::hash() const ../src/util/obj_hashtable.h:76
......
SUMMARY: AddressSanitizer: heap-use-after-free ../src/ast/ast.h:503 in ast::hash() const
Shadow bytes around the buggy address:
  0x0c0c80004500: fd fd fd fa fa fa fa fa 00 00 00 00 00 00 00 00
  0x0c0c80004510: fa fa fa fa 00 00 00 00 00 00 00 04 fa fa fa fa
  0x0c0c80004520: 00 00 00 00 00 00 00 04 fa fa fa fa fd fd fd fd
  0x0c0c80004530: fd fd fd fa fa fa fa fa fd fd fd fd fd fd fd fd
  0x0c0c80004540: fa fa fa fa fd fd fd fd fd fd fd fd fa fa fa fa
=>0x0c0c80004550: 00 00 00 00 00 00 00 04 fa fa fa fa fd[fd]fd fd
  0x0c0c80004560: fd fd fd fd fa fa fa fa fd fd fd fd fd fd fd fd
  0x0c0c80004570: fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa
  0x0c0c80004580: fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa
  0x0c0c80004590: fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa
  0x0c0c800045a0: fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa
Shadow byte legend (one shadow byte represents 8 application bytes):
  Addressable:           00
  Partially addressable: 01 02 03 04 05 06 07
  Heap left redzone:       fa
  Freed heap region:       fd
  Stack left redzone:      f1
  Stack mid redzone:       f2
  Stack right redzone:     f3
  Stack after return:      f5
  Stack use after scope:   f8
  Global redzone:          f9
  Global init order:       f6
  Poisoned by user:        f7
  Container overflow:      fc
  Array cookie:            ac
  Intra object redzone:    bb
  ASan internal:           fe
  Left alloca redzone:     ca
  Right alloca redzone:    cb
  Shadow gap:              cc
==210252==ABORTING