Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

heap-use-after-free at src/ast/ast.h:507:36 #6914

Closed
merlinsun opened this issue Sep 22, 2023 · 0 comments
Closed

heap-use-after-free at src/ast/ast.h:507:36 #6914

merlinsun opened this issue Sep 22, 2023 · 0 comments

Comments

@merlinsun
Copy link

Hi,
For this instance, z3 fba5de3

$ cat small.smt2 
(declare-fun b (Int) Bool)
(assert (exists ((r String)) (distinct (- 1) (str.to_int (str.substr r 1 1)))))
(assert (forall ((v Int)) (exists ((a Int)) (not (b (+ 1 v))))))
(check-sat)
$ z3asan small.smt2 
=================================================================
==27873==ERROR: AddressSanitizer: heap-use-after-free on address 0x60700004f16c at pc 0x0000005e3867 bp 0x7ffd9c40eaf0 sp 0x7ffd9c40eae8
READ of size 4 at 0x60700004f16c thread T0
    #0 0x5e3866 in ast::hash() const /root/z3/build/../src/ast/ast.h:507:36
    #1 0x6eabdf in obj_map<expr, expr*>::key_data::hash() const /root/z3/build/../src/util/obj_hashtable.h:76:47
    #2 0x6eaae4 in obj_map<expr, expr*>::obj_map_entry::get_hash() const /root/z3/build/../src/util/obj_hashtable.h:84:51
......

SUMMARY: AddressSanitizer: heap-use-after-free /root/z3/build/../src/ast/ast.h:507:36 in ast::hash() const
......
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant