Segment fault at model_evaluator.cpp:634 (opt.priority pareto, uto_config false, smt.case_split 4)

[rainoftime]

Hi, for the following formula,

(set-logic QF_ABV)
(set-option :opt.priority pareto)
(set-option :auto_config false)
(set-option :smt.case_split 4)
(declare-const bv_30-0 (_ BitVec 30))
(declare-const bv_31-0 (_ BitVec 31))
(maximize bv_30-0)
(minimize bv_31-0)
(check-sat)

z3 (commit 1f15033) throws a seg fault

ASAN:SIGSEGV
=================================================================
==116846==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000080 (pc 0x000001a77438 bp 0x7ffe17a51340 sp 0x7ffe17a51310 T0)
    #0 0x1a77437 in model_evaluator::set_model_completion(bool) ../src/model/model_evaluator.cpp:634
    #1 0x5331d0 in model::set_model_completion(bool) ../src/model/model.h:94
    #2 0x5a5193 in opt::gia_pareto::operator()() ../src/opt/opt_pareto.cpp:44
    #3 0x57f2a8 in opt::context::execute_pareto() ../src/opt/opt_context.cpp:606
    #4 0x57bef8 in opt::context::optimize(ref_vector<expr, ast_manager> const&) ../src/opt/opt_context.cpp:339
    #5 0x196aaa1 in cmd_context::check_sat(unsigned int, expr* const*) ../src/cmd_context/cmd_context.cpp:1525
    #6 0x18fb499 in smt2::parser::parse_check_sat() ../src/parsers/smt2/smt2parser.cpp:2596
    #7 0x18ff3f5 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2938
    #8 0x1900b07 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3130
    #9 0x18dfb2c in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3179
    #10 0x43c162 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:89
    #11 0x454292 in main ../src/shell/main.cpp:352
    #12 0x7f203d73482f in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x2082f)
    #13 0x414ba8 in _start (/home/peisen/test/tofuzz/z3-debug/build/z3+0x414ba8)

AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV ../src/model/model_evaluator.cpp:634 model_evaluator::set_model_completion(bool)
==116846==ABORTING