search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.29k stars 1.48k forks source link

SEGV at smt::theory::get_family_id() #3598

Closed rainoftime closed 4 years ago

rainoftime commented 4 years ago

Hi, for the following formula

(set-logic QF_ABV)
(set-option :opt.maxsat_engine wmax)
(set-option :smt.random_seed 1)
(set-option :smt.threads 5)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v5 Bool)
(declare-const v8 Bool)
(declare-const bv_19-0 (_ BitVec 19))
(declare-const v12 Bool)
(assert-soft (or (distinct (bvsle #b0111111110 #b0111111110) v8 v2) v12))
(assert-soft (or (= bv_19-0 (bvurem bv_19-0 bv_19-0) bv_19-0 (bvurem bv_19-0 bv_19-0) (bvurem bv_19-0 bv_19-0))))
(assert-soft (or v5))
(check-sat)

asan detects a SEGV in z3 (commit 7f8738dd85)

=================================================================
==23264==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000008 (pc 0x000000e88553 bp 0x7ffd4024a890 sp 0x7ffd4024a880 T0)
==23264==The signal is caused by a READ memory access.
==23264==Hint: address points to the zero page.
    #0 0xe88552 in smt::theory::get_family_id() const (/home/rainoftime/Work/tofuzz/z3/build/z3+0xe88552)
    #1 0xe6b6e1 in smt::context::register_plugin(smt::theory*) ../src/smt/smt_context.cpp:2872
    #2 0xe4b4f9 in smt::context::copy_plugins(smt::context&, smt::context&) ../src/smt/smt_context.cpp:255
    #3 0xe4a6b6 in smt::context::copy(smt::context&, smt::context&, bool) ../src/smt/smt_context.cpp:174
    #4 0x10bda98 in smt::parallel::operator()(ref_vector<expr, ast_manager> const&) ../src/smt/smt_parallel.cpp:66
    #5 0xe754b9 in smt::context::check(unsigned int, expr* const*, bool) ../src/smt/smt_context.cpp:3524
    #6 0xe4765c in smt::kernel::imp::check(unsigned int, expr* const*) ../src/smt/smt_kernel.cpp:116
    #7 0xe45f47 in smt::kernel::check(unsigned int, expr* const*) ../src/smt/smt_kernel.cpp:296
    #8 0x5d8341 in opt::opt_solver::check_sat_core2(unsigned int, expr* const*) ../src/opt/opt_solver.cpp:186
    #9 0x1d8e183 in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67
    #10 0x1d85733 in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:330
    #11 0x615e84 in opt::wmax::operator()() (/home/rainoftime/Work/tofuzz/z3/build/z3+0x615e84)
    #12 0x5e77e3 in opt::maxsmt::operator()() ../src/opt/maxsmt.cpp:263
    #13 0x5a72f3 in opt::context::execute_maxsat(symbol const&, bool, bool) ../src/opt/opt_context.cpp:423
    #14 0x5a7637 in opt::context::execute(opt::context::objective const&, bool, bool) ../src/opt/opt_context.cpp:437
    #15 0x5a5d98 in opt::context::optimize(ref_vector<expr, ast_manager> const&) ../src/opt/opt_context.cpp:332
    #16 0x1d354b7 in cmd_context::check_sat(unsigned int, expr* const*) ../src/cmd_context/cmd_context.cpp:1557
    #17 0x1cb383d in smt2::parser::parse_check_sat() ../src/parsers/smt2/smt2parser.cpp:2596
    #18 0x1cb7c96 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2938
    #19 0x1cb94a3 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3130
    #20 0x1c9342a in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3179
    #21 0x46f5a1 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:89
    #22 0x4598ac in main ../src/shell/main.cpp:352
    #23 0x7f7f1741a82f in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x2082f)
NikolajBjorner commented 4 years ago

your efforts are appreciated, but there are too many feature overload abuse bugs being filed. They seem a waste of time to consider as they are progressively unlikely to correspond to reasonable use cases.