heap-use-after-free on string formula at ast.h:502

[rainoftime]

Hi, for the following formula, z3 a11ca1a

(declare-fun x () (Seq (Seq Int)))
(declare-fun xp () (Seq (Seq Int)))
(declare-fun z () (Seq Int))
(declare-fun n () Int)
(declare-fun l0 () Bool)
(declare-fun l1 () Bool)
(declare-fun l3 () Bool)
(declare-fun l4 () Bool)
(declare-fun l5 () Bool)
(assert (not (= (seq.unit 1) (seq.extract z 0 1))))
(assert (= l5 l0))
(assert (not (= (seq.extract z n 1) (seq.unit 0))))
(assert (= l4 (= x (seq.++ xp (seq.unit z)))))
(check-sat-assuming (l1 l3 l5))
(check-sat-assuming (l4))

sat
unknown
=================================================================
==128456==ERROR: AddressSanitizer: heap-use-after-free on address 0x607000063ae4 at pc 0x0000005bde37 bp 0x7fffaa6ad170 sp 0x7fffaa6ad168
READ of size 4 at 0x607000063ae4 thread T0
    #0 0x5bde36 in ast::hash() const /home/z3-debug/build/../src/ast/ast.h:502:36
    #1 0x8c3753 in obj_ptr_pair_hash<expr, expr>::operator()(std::pair<expr*, expr*> const&) const /home/z3-debug/build/..
/src/util/hash.h:176:38
    #2 0x8c359f in core_hashtable<obj_pair_hash_entry<expr, expr>, obj_ptr_pair_hash<expr, expr>, default_eq<std::pair<expr*, expr*> > >::get
_hash(std::pair<expr*, expr*> const&) const /home/z3-debug/build/../src/util/hashtable.h:152:64
    #3 0x2328436 in core_hashtable<obj_pair_hash_entry<expr, expr>, obj_ptr_pair_hash<expr, expr>, default_eq<std::pair<expr*, expr*> > >::re
move(std::pair<expr*, expr*> const&) /home/z3-debug/build/../src/util/hashtable.h:558:25
    #4 0x2308cac in core_hashtable<obj_pair_hash_entry<expr, expr>, obj_ptr_pair_hash<expr, expr>, default_eq<std::pair<expr*, expr*> > >::er
ase(std::pair<expr*, expr*> const&) /home/z3-debug/build/../src/util/hashtable.h:591:34
    #5 0x2427bf7 in remove_obj_pair_map::undo() /home/z3-debug/build/../src/smt/seq_eq_solver.cpp:1125:15
    #6 0x107c87f in undo_trail_stack(ptr_vector<trail>&, unsigned int) /home/z3-debug/build/../src/util/trail.h:388:16

[NikolajBjorner]

It would be productive to check regressions by having an GitHub Action in z3test repository that reproduces steps of these crashes. That is, I don't have your Asan environment handy and can mainly guess what the issue is based on this trail.
There is one Action already under z3test that runs over consolidated issues. A drawback of the regression test script we use is that it hides some error messages so it would likely use some other mechanism to be useful.

[NikolajBjorner]

I guess it is fixed.