Use after Free in get_failed_assumptions

While fuzzing boolector,

this input file

``` (assert#b0) (check-sat) (get-unsat-assumptions) (get-unsat-assumptions) ```

was found, which leads to a use after free in get_failed_assumptions.

The input file looks like this is related to #28, but the backtrace produced by ASAN is different, which is why this is filed as a separate issue.

The attached file contains more lines leading to the same crash, the above file contains the minimal version.

ASAN trace

``` ================================================================= ==9780==ERROR: AddressSanitizer: heap-use-after-free on address 0x602000009710 at pc 0x00000052bd1c bp 0x7ffd2e8c9eb0 sp 0x7ffd2e8c9ea8 READ of size 8 at 0x602000009710 thread T0 #0 0x52bd1b in boolector_get_failed_assumptions /home/user/boolector-master/src/boolector.c:624:12 #1 0x6851db in read_command_smt2 /home/user/boolector-master/src/parser/btorsmt2.c:4700:28 #2 0x682a27 in parse_smt2_parser /home/user/boolector-master/src/parser/btorsmt2.c:4828:10 #3 0x5a033a in parse_aux /home/user/boolector-master/src/btorparse.c:68:15 #4 0x59f55a in btor_parse /home/user/boolector-master/src/btorparse.c:230:9 #5 0x52531e in boolector_main /home/user/boolector-master/src/btormain.c:1454:19 #6 0x7f53f5a65b96 in __libc_start_main /build/glibc-OTsEL5/glibc-2.27/csu/../csu/libc-start.c:310 #7 0x4367a9 in _start (/home/user/boolector-asan+0x4367a9) 0x602000009710 is located 0 bytes inside of 8-byte region [0x602000009710,0x602000009718) freed by thread T0 here: #0 0x4e5bc8 in __interceptor_free.localalias.0 (/home/user/boolector-asan+0x4e5bc8) #1 0x68525b in read_command_smt2 /home/user/boolector-master/src/parser/btorsmt2.c:4706:7 #2 0x682a27 in parse_smt2_parser /home/user/boolector-master/src/parser/btorsmt2.c:4828:10 #3 0x5a033a in parse_aux /home/user/boolector-master/src/btorparse.c:68:15 #4 0x59f55a in btor_parse /home/user/boolector-master/src/btorparse.c:230:9 #5 0x52531e in boolector_main /home/user/boolector-master/src/btormain.c:1454:19 #6 0x7f53f5a65b96 in __libc_start_main /build/glibc-OTsEL5/glibc-2.27/csu/../csu/libc-start.c:310 previously allocated by thread T0 here: #0 0x4e61a5 in realloc (/home/user/boolector-asan+0x4e61a5) #1 0x6cd24e in btor_mem_realloc /home/user/boolector-master/src/utils/btormem.c:104:12 #2 0x52bc11 in boolector_get_failed_assumptions /home/user/boolector-master/src/boolector.c:633:3 #3 0x6851db in read_command_smt2 /home/user/boolector-master/src/parser/btorsmt2.c:4700:28 #4 0x682a27 in parse_smt2_parser /home/user/boolector-master/src/parser/btorsmt2.c:4828:10 #5 0x5a033a in parse_aux /home/user/boolector-master/src/btorparse.c:68:15 #6 0x59f55a in btor_parse /home/user/boolector-master/src/btorparse.c:230:9 #7 0x52531e in boolector_main /home/user/boolector-master/src/btormain.c:1454:19 #8 0x7f53f5a65b96 in __libc_start_main /build/glibc-OTsEL5/glibc-2.27/csu/../csu/libc-start.c:310 SUMMARY: AddressSanitizer: heap-use-after-free /home/user/boolector-master/src/boolector.c:624:12 in boolector_get_failed_assumptions Shadow bytes around the buggy address: 0x0c047fff9290: fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa 0x0c047fff92a0: fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa 0x0c047fff92b0: fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa 0x0c047fff92c0: fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa 0x0c047fff92d0: fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa =>0x0c047fff92e0: fa fa[fd]fa fa fa 00 fa fa fa fd fd fa fa fd fa 0x0c047fff92f0: fa fa fd fd fa fa fd fd fa fa fd fa fa fa fd fa 0x0c047fff9300: fa fa fd fa fa fa fd fa fa fa 04 fa fa fa 04 fa 0x0c047fff9310: fa fa 05 fa fa fa 03 fa fa fa 06 fa fa fa 06 fa 0x0c047fff9320: fa fa 00 01 fa fa 00 01 fa fa 00 01 fa fa 00 01 0x0c047fff9330: fa fa 00 fa fa fa 06 fa fa fa 07 fa fa fa 07 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 Heap right redzone: fb Freed heap region: fd Stack left redzone: f1 Stack mid redzone: f2 Stack right redzone: f3 Stack partial redzone: f4 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 ==9780==ABORTING ```

Valgrind trace

``` ==9802== Memcheck, a memory error detector ==9802== Copyright (C) 2002-2017, and GNU GPL'd, by Julian Seward et al. ==9802== Using Valgrind-3.13.0 and LibVEX; rerun with -h for copyright info ==9802== Command: ./boolector-plain boolector_get_failed_assumptions.txt ==9802== ==9802== Invalid read of size 8 ==9802== at 0x12B0AD: boolector_get_failed_assumptions (in /home/user/boolector-plain) ==9802== by 0x1CA6D2: read_command_smt2 (in /home/user/boolector-plain) ==9802== by 0x1CC289: parse_smt2_parser (in /home/user/boolector-plain) ==9802== by 0x16C6FD: btor_parse (in /home/user/boolector-plain) ==9802== by 0x128F87: boolector_main (in /home/user/boolector-plain) ==9802== by 0x541AB96: (below main) (libc-start.c:310) ==9802== Address 0x5809830 is 0 bytes inside a block of size 8 free'd ==9802== at 0x4C30D3B: free (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so) ==9802== by 0x1CA705: read_command_smt2 (in /home/user/boolector-plain) ==9802== by 0x1CC289: parse_smt2_parser (in /home/user/boolector-plain) ==9802== by 0x16C6FD: btor_parse (in /home/user/boolector-plain) ==9802== by 0x128F87: boolector_main (in /home/user/boolector-plain) ==9802== by 0x541AB96: (below main) (libc-start.c:310) ==9802== Block was alloc'd at ==9802== at 0x4C2FA3F: malloc (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so) ==9802== by 0x4C31D84: realloc (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so) ==9802== by 0x1D906D: btor_mem_realloc (in /home/user/boolector-plain) ==9802== by 0x12B1B2: boolector_get_failed_assumptions (in /home/user/boolector-plain) ==9802== by 0x1CA6D2: read_command_smt2 (in /home/user/boolector-plain) ==9802== by 0x1CC289: parse_smt2_parser (in /home/user/boolector-plain) ==9802== by 0x16C6FD: btor_parse (in /home/user/boolector-plain) ==9802== by 0x128F87: boolector_main (in /home/user/boolector-plain) ==9802== by 0x541AB96: (below main) (libc-start.c:310) ==9802== ==9802== Invalid free() / delete / delete[] / realloc() ==9802== at 0x4C30D3B: free (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so) ==9802== by 0x12B10A: boolector_get_failed_assumptions (in /home/user/boolector-plain) ==9802== by 0x1CA6D2: read_command_smt2 (in /home/user/boolector-plain) ==9802== by 0x1CC289: parse_smt2_parser (in /home/user/boolector-plain) ==9802== by 0x16C6FD: btor_parse (in /home/user/boolector-plain) ==9802== by 0x128F87: boolector_main (in /home/user/boolector-plain) ==9802== by 0x541AB96: (below main) (libc-start.c:310) ==9802== Address 0x5809830 is 0 bytes inside a block of size 8 free'd ==9802== at 0x4C30D3B: free (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so) ==9802== by 0x1CA705: read_command_smt2 (in /home/user/boolector-plain) ==9802== by 0x1CC289: parse_smt2_parser (in /home/user/boolector-plain) ==9802== by 0x16C6FD: btor_parse (in /home/user/boolector-plain) ==9802== by 0x128F87: boolector_main (in /home/user/boolector-plain) ==9802== by 0x541AB96: (below main) (libc-start.c:310) ==9802== Block was alloc'd at ==9802== at 0x4C2FA3F: malloc (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so) ==9802== by 0x4C31D84: realloc (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so) ==9802== by 0x1D906D: btor_mem_realloc (in /home/user/boolector-plain) ==9802== by 0x12B1B2: boolector_get_failed_assumptions (in /home/user/boolector-plain) ==9802== by 0x1CA6D2: read_command_smt2 (in /home/user/boolector-plain) ==9802== by 0x1CC289: parse_smt2_parser (in /home/user/boolector-plain) ==9802== by 0x16C6FD: btor_parse (in /home/user/boolector-plain) ==9802== by 0x128F87: boolector_main (in /home/user/boolector-plain) ==9802== by 0x541AB96: (below main) (libc-start.c:310) ==9802== ==9802== Invalid read of size 8 ==9802== at 0x14BC53: btor_delete (in /home/user/boolector-plain) ==9802== by 0x127EC9: boolector_main (in /home/user/boolector-plain) ==9802== by 0x541AB96: (below main) (libc-start.c:310) ==9802== Address 0x5809880 is 0 bytes inside a block of size 8 free'd ==9802== at 0x4C30D3B: free (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so) ==9802== by 0x1CA705: read_command_smt2 (in /home/user/boolector-plain) ==9802== by 0x1CC289: parse_smt2_parser (in /home/user/boolector-plain) ==9802== by 0x16C6FD: btor_parse (in /home/user/boolector-plain) ==9802== by 0x128F87: boolector_main (in /home/user/boolector-plain) ==9802== by 0x541AB96: (below main) (libc-start.c:310) ==9802== Block was alloc'd at ==9802== at 0x4C2FA3F: malloc (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so) ==9802== by 0x4C31D84: realloc (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so) ==9802== by 0x1D906D: btor_mem_realloc (in /home/user/boolector-plain) ==9802== by 0x12B1B2: boolector_get_failed_assumptions (in /home/user/boolector-plain) ==9802== by 0x1CA6D2: read_command_smt2 (in /home/user/boolector-plain) ==9802== by 0x1CC289: parse_smt2_parser (in /home/user/boolector-plain) ==9802== by 0x16C6FD: btor_parse (in /home/user/boolector-plain) ==9802== by 0x128F87: boolector_main (in /home/user/boolector-plain) ==9802== by 0x541AB96: (below main) (libc-start.c:310) ==9802== ==9802== Invalid free() / delete / delete[] / realloc() ==9802== at 0x4C30D3B: free (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so) ==9802== by 0x14BC8E: btor_delete (in /home/user/boolector-plain) ==9802== by 0x127EC9: boolector_main (in /home/user/boolector-plain) ==9802== by 0x541AB96: (below main) (libc-start.c:310) ==9802== Address 0x5809880 is 0 bytes inside a block of size 8 free'd ==9802== at 0x4C30D3B: free (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so) ==9802== by 0x1CA705: read_command_smt2 (in /home/user/boolector-plain) ==9802== by 0x1CC289: parse_smt2_parser (in /home/user/boolector-plain) ==9802== by 0x16C6FD: btor_parse (in /home/user/boolector-plain) ==9802== by 0x128F87: boolector_main (in /home/user/boolector-plain) ==9802== by 0x541AB96: (below main) (libc-start.c:310) ==9802== Block was alloc'd at ==9802== at 0x4C2FA3F: malloc (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so) ==9802== by 0x4C31D84: realloc (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so) ==9802== by 0x1D906D: btor_mem_realloc (in /home/user/boolector-plain) ==9802== by 0x12B1B2: boolector_get_failed_assumptions (in /home/user/boolector-plain) ==9802== by 0x1CA6D2: read_command_smt2 (in /home/user/boolector-plain) ==9802== by 0x1CC289: parse_smt2_parser (in /home/user/boolector-plain) ==9802== by 0x16C6FD: btor_parse (in /home/user/boolector-plain) ==9802== by 0x128F87: boolector_main (in /home/user/boolector-plain) ==9802== by 0x541AB96: (below main) (libc-start.c:310) ==9802== ==9802== ==9802== HEAP SUMMARY: ==9802== in use at exit: 0 bytes in 0 blocks ==9802== total heap usage: 1,164 allocs, 1,166 frees, 46,991 bytes allocated ==9802== ==9802== All heap blocks were freed -- no leaks are possible ==9802== ==9802== For counts of detected and suppressed errors, rerun with: -v ==9802== ERROR SUMMARY: 4 errors from 4 contexts (suppressed: 0 from 0) ```

Used version

$ boolector --version
3.0.1-pre

Steps to reproduce

boolector  boolector_get_failed_assumptions.txt

Boolector / boolector

Use after Free in get_failed_assumptions #29