Closed wcventure closed 5 years ago
This issue concerns the SMT-LIB v1 parser. SMT-LIB v1 is outdated, SMT-LIB v2 is the current standard. We do not actively support and maintain Boolector's parser for SMT-LIB v1 and thus won't fix this issue. Support for parsing SMT-LIB v1 input will be removed some time in the future.
Hi, there.
A Use-after-free problem was discovered in car function in btorsmt.c in src/parser. A crafted input can cause segment faults and I have confirmed them with address sanitizer too.
Here are the POC files. Please use
./boolector $POC
to reproduce the bug. POC.zipNote that similar issues were reported (#28 and #29) in the past, which is fixed. But this bug can still reproduce on the master branch.
$ git log
The ASAN dumps the stack trace as follows: