search

Z3Prover / z3

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

seg fault at ../src/model/model.cpp:77 #3664

Closed rainoftime closed 4 years ago

rainoftime commented 4 years ago

Hi, For the following formula

(set-logic QF_BV)
(set-option :opt.dump_models true)
(set-option :model_validate true)
(set-option :model true)
(set-option :sat.prob_search true)
(set-option :sat.xor.solver true)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const bv_24-0 (_ BitVec 24))
(declare-const bv_5-0 (_ BitVec 5))
(declare-const v11 Bool)
(push 1)
(pop 1)
(declare-const v12 Bool)
(declare-const v13 Bool)
(declare-const v14 Bool)
(declare-const v15 Bool)
(assert (or v4 v5 v14))
(assert (or (distinct (bvlshr bv_24-0 bv_24-0) (bvlshr bv_24-0 bv_24-0)) (distinct (bvlshr bv_24-0 bv_24-0) (bvlshr bv_24-0 bv_24-0)) v7))
(assert (or v11 v12 (distinct (bvlshr bv_24-0 bv_24-0) (bvlshr bv_24-0 bv_24-0))))
(assert (or (not (or v3 v3 v0 v7 v10 v1 v0)) v1 v12))
(assert (or v14 v4 (distinct (bvsrem #xe5 #xe5) #xe5)))
(maximize bv_5-0)
(maximize bv_24-0)
(check-sat)

asan detects a SEGV in z3 Commit: 65b2037

==27351==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000008 (pc 0x000001e6a9af bp 0x7ffc24954470 sp 0x7ffc24954430 T0)
==27351==The signal is caused by a READ memory access.
==27351==Hint: address points to the zero page.
    #0 0x1e6a9ae in model::copy() const ../src/model/model.cpp:77
    #1 0x5a6750 in opt::context::set_model(ref<model>&) ../src/opt/opt_context.cpp:378
    #2 0x5b2455 in opt::context::model_updated(model*) ../src/opt/opt_context.cpp:1093
    #3 0x5a5aba in opt::context::optimize(ref_vector<expr, ast_manager> const&) ../src/opt/opt_context.cpp:307
    #4 0x1d3e119 in cmd_context::check_sat(unsigned int, expr* const*) ../src/cmd_context/cmd_context.cpp:1557
    #5 0x1cbc49f in smt2::parser::parse_check_sat() ../src/parsers/smt2/smt2parser.cpp:2596
    #6 0x1cc08f8 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2938
    #7 0x1cc2105 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3130
    #8 0x1c9c08c in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3179
    #9 0x46f791 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:89
    #10 0x459a9c in main ../src/shell/main.cpp:352
    #11 0x7f4412fea82f in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x2082f)
NikolajBjorner commented 4 years ago

dup