Boolector / boolector

A Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions.
http://boolector.github.io
Other
325 stars 63 forks source link

Segment fault at btorexp.c:1116 #103

Closed rainoftime closed 4 years ago

rainoftime commented 4 years ago

Hi, for the following formula,

(set-logic BV)
(declare-const bv_28-0 (_ BitVec 28))
(assert (not (forall ((q4 (_ BitVec 28)) (q5 (_ BitVec 12))) (not (= (bvshl bv_28-0 bv_28-0) q4 bv_28-0 q4)))))
(check-sat)

boolector (commit 76aafdf) throws a seg fault

ASAN:SIGSEGV
=================================================================
==30226==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000030 (pc 0x7f8cdce46bc1 bp 0x7ffef5b2ff30 sp 0x7ffef5b2ff00 T0)
    #0 0x7f8cdce46bc0 in btor_exp_bv_sll /home/peisen/test/tofuzz/boolector/src/btorexp.c:1116
    #1 0x7f8cdce41259 in btor_exp_create /home/peisen/test/tofuzz/boolector/src/btorexp.c:48
    #2 0x7f8cdd01e281 in elim_vars /home/peisen/test/tofuzz/boolector/src/preprocess/btorder.c:401
    #3 0x7f8cdd01e9c8 in btor_cer_node /home/peisen/test/tofuzz/boolector/src/preprocess/btorder.c:445
    #4 0x7f8cdcf3beea in simplify /home/peisen/test/tofuzz/boolector/src/btorslvquant.c:2587
    #5 0x7f8cdcf3c151 in sat_quant_solver /home/peisen/test/tofuzz/boolector/src/btorslvquant.c:2611
    #6 0x7f8cdce3551c in btor_check_sat /home/peisen/test/tofuzz/boolector/src/btorcore.c:3036
    #7 0x7f8cdcd3396f in boolector_sat /home/peisen/test/tofuzz/boolector/src/boolector.c:639
    #8 0x7f8cdd00ef90 in check_sat /home/peisen/test/tofuzz/boolector/src/parser/btorsmt2.c:4529
    #9 0x7f8cdd012a0b in read_command_smt2 /home/peisen/test/tofuzz/boolector/src/parser/btorsmt2.c:4695
    #10 0x7f8cdd015937 in parse_smt2_parser /home/peisen/test/tofuzz/boolector/src/parser/btorsmt2.c:4952
    #11 0x7f8cdce8eeae in parse_aux /home/peisen/test/tofuzz/boolector/src/btorparse.c:68
    #12 0x7f8cdce90ae6 in btor_parse /home/peisen/test/tofuzz/boolector/src/btorparse.c:235
    #13 0x7f8cdcd9daeb in boolector_parse /home/peisen/test/tofuzz/boolector/src/boolector.c:4680
    #14 0x40cb32 in boolector_main /home/peisen/test/tofuzz/boolector/src/btormain.c:1440
    #15 0x4024f5 in main /home/peisen/test/tofuzz/boolector/src/boolectormain.c:17
    #16 0x7f8cdc89b82f in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x2082f)
    #17 0x402408 in _start (/home/peisen/test/tofuzz/boolector/build/bin/boolector+0x402408)

AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV /home/peisen/test/tofuzz/boolector/src/btorexp.c:1116 btor_exp_bv_sll
==30226==ABORTING
mpreiner commented 4 years ago

Duplicate #97.