search

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
332 stars 62 forks source link

SMT2: Calling `assert` between `check-sat` and `get-value` causes crash instead of error #65

Closed mateon1 closed 5 years ago

mateon1 commented 5 years ago

The following SMT2 file causes a crash:

(set-option :produce-models true )
(set-logic QF_BV )

(declare-fun dummy () (_ BitVec 8))
(assert (not (= dummy #x42)))
(check-sat)
(assert (= dummy #x00))
(get-value (dummy))

On release builds this derefs a null pointer, on debug builds this causes an assertion failure.

Backtrace on debug build:

#0  raise (sig=6) at ../sysdeps/unix/sysv/linux/raise.c:50
#1  0x0000000000401add in abort ()
#2  0x00000000004019b7 in __assert_fail_base.cold.0 ()
#3  0x00000000006e8132 in __assert_fail ()
#4  0x000000000048439c in btor_model_get_bv_aux (btor=0x895840, bv_model=0x0, fun_model=0x0, exp=0x8ac160) at /shared/dev/boolector/src/btormodel.c:508
#5  0x00000000004845aa in btor_model_get_bv (btor=0x895840, exp=0x8ac160) at /shared/dev/boolector/src/btormodel.c:569
#6  0x000000000049defd in print_bv_value_smt2 (btor=0x895840, node=0x8ac160, symbol_str=0x8bfc60 "in1a", base=1, file=0x8789e0 <_IO_2_1_stdout_>)
    at /shared/dev/boolector/src/btorprintmodel.c:417
#7  0x000000000049e4aa in btor_print_value_smt2 (btor=0x895840, exp=0x8ac160, symbol_str=0x8bfc60 "in1a", file=0x8789e0 <_IO_2_1_stdout_>)
    at /shared/dev/boolector/src/btorprintmodel.c:512
#8  0x000000000040c30c in boolector_print_value_smt2 (btor=0x895840, node=0x8ac160, symbol_str=0x8bfc60 "in1a", file=0x8789e0 <_IO_2_1_stdout_>)
    at /shared/dev/boolector/src/boolector.c:310
#9  0x0000000000573b8f in read_command_smt2 (parser=0x89bec0) at /shared/dev/boolector/src/parser/btorsmt2.c:4771
#10 0x00000000005741b4 in parse_smt2_parser (parser=0x89bec0, prefix=0x7fffffffe740, infile=0x89bc50, infile_name=0x7fffffffed83 "/tmp/manual.smt2", 
    outfile=0x8789e0 <_IO_2_1_stdout_>, res=0x7fffffffe6b0) at /shared/dev/boolector/src/parser/btorsmt2.c:4862
#11 0x000000000049abaa in parse_aux (btor=0x895840, infile=0x89bc50, prefix=0x7fffffffe740, infile_name=0x7fffffffed83 "/tmp/manual.smt2", 
    outfile=0x8789e0 <_IO_2_1_stdout_>, parser_api=0x877310 <parsesmt2_parser_api>, error_msg=0x7fffffffe918, status=0x7fffffffe924, 
    msg=0x89be80 "parsing '/tmp/manual.smt2'") at /shared/dev/boolector/src/btorparse.c:68
#12 0x000000000049bf3e in btor_parse (btor=0x895840, infile=0x89bc50, infile_name=0x7fffffffed83 "/tmp/manual.smt2", outfile=0x8789e0 <_IO_2_1_stdout_>, 
    error_msg=0x7fffffffe918, status=0x7fffffffe924) at /shared/dev/boolector/src/btorparse.c:230
#13 0x000000000043d495 in boolector_parse (btor=0x895840, infile=0x89bc50, infile_name=0x7fffffffed83 "/tmp/manual.smt2", outfile=0x8789e0 <_IO_2_1_stdout_>, 
    error_msg=0x7fffffffe918, status=0x7fffffffe924) at /shared/dev/boolector/src/boolector.c:4612
#14 0x000000000040a1d8 in boolector_main (argc=2, argv=0x7fffffffeb18) at /shared/dev/boolector/src/btormain.c:1462
#15 0x00000000004036bd in main (argc=2, argv=0x7fffffffeb18) at /shared/dev/boolector/src/boolectormain.c:17
mpreiner commented 5 years ago

You are right, Boolector should actually print a warning/error since the (get-value ...) is not issued in sat mode.