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

ASAN memory leak at Theory.cc:123 #69

Closed
rainoftime opened this issue Mar 29, 2020 · 1 comment · Fixed by #86
Closed

ASAN memory leak at Theory.cc:123 #69

rainoftime opened this issue Mar 29, 2020 · 1 comment · Fixed by #86

Comments

@rainoftime
Copy link

Hi, for the following formula

(set-logic QF_LIA)
(check-sat)
(assert false)
(check-sat)
(check-sat)

ASAN detects a memory leak in opensmt (commit e9e14b4)

==11477==ERROR: LeakSanitizer: detected memory leaks                                                                                   [83/101]

Direct leak of 504 byte(s) in 1 object(s) allocated from:
    #0 0x7f94acb6d658 in operator new[](unsigned long) (/usr/lib/x86_64-linux-gnu/libasan.so.4+0xe0658)
    #1 0x586b29 in Map<PTRef, lbool, PTRefHash, Equal<PTRef> >::rehash() /home/rainoftime/Work/tofuzz/opensmt/src/minisat/mtl/Map.h:87
    #2 0x57f36a in Map<PTRef, lbool, PTRefHash, Equal<PTRef> >::insert(PTRef const&, lbool const&) /home/rainoftime/Work/tofuzz/opensmt/src/min
isat/mtl/Map.h:138
    #3 0x5bfa80 in Theory::computeSubstitutions(PTRef, vec<PFRef> const&, int) /home/rainoftime/Work/tofuzz/opensmt/src/logics/Theory.cc:123
    #4 0x66f69f in LIATheory::simplify(vec<PFRef> const&, int) /home/rainoftime/Work/tofuzz/opensmt/src/logics/LIATheory.cc:21
    #5 0x4baf0f in MainSolver::simplifyFormulas(char**) /home/rainoftime/Work/tofuzz/opensmt/src/api/MainSolver.cc:115
    #6 0x4b27ee in MainSolver::simplifyFormulas() /home/rainoftime/Work/tofuzz/opensmt/src/api/MainSolver.h:178
    #7 0x4be392 in MainSolver::check() /home/rainoftime/Work/tofuzz/opensmt/src/api/MainSolver.cc:366
    #8 0x4a842f in Interpret::checkSat() /home/rainoftime/Work/tofuzz/opensmt/src/api/Interpret.cc:697
    #9 0x4a4e9d in Interpret::interp(ASTNode&) /home/rainoftime/Work/tofuzz/opensmt/src/api/Interpret.cc:415
    #10 0x4ad480 in Interpret::execute(ASTNode const*) /home/rainoftime/Work/tofuzz/opensmt/src/api/Interpret.cc:1044
    #11 0x4ad680 in Interpret::interpFile(_IO_FILE*) /home/rainoftime/Work/tofuzz/opensmt/src/api/Interpret.cc:1057
    #12 0x49cf4a in main /home/rainoftime/Work/tofuzz/opensmt/src/bin/opensmt.cc:129
    #13 0x7f94ab4f682f in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x2082f)
@blishko
Copy link
Member

blishko commented Apr 4, 2020

Same problem as in #70

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

Successfully merging a pull request may close this issue.

2 participants