(purify-arith smt) Invalid model for formula with rem

[rainoftime]

Hi, for the following formula, z3 c959e28

(assert (let (($x20 (> 0 (rem 0 0))))))
(check-sat-using (then purify-arith smt))

z3 model_validate=true delta.out.smt2
sat
(error "line 2 column 40: an invalid model was generated")

[rainoftime]

(simplify 1 :print-proofs true)

==183994==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000004 (pc 0x000000479a8d bp 0x7ffe2b14c0f0 sp 0x7ffe2b14c0e0 T0)
    #0 0x479a8c in ast::get_kind() const ../src/ast/ast.h:508
    #1 0x24bb7bb in smt_printer::operator()(expr*) ../src/ast/ast_smt_pp.cpp:748
    #2 0x24b4515 in ast_smt_pp::display_expr_smt2(std::ostream&, expr*, unsigned int, unsigned int, char const* const*) ../src/ast/ast_smt_pp.cpp:915
    #3 0x1b4b241 in simplify_cmd::execute(cmd_context&) ../src/cmd_context/simplify_cmd.cpp:110
    #4 0x1b0b2cf in smt2::parser::parse_ext_cmd(int, int) ../src/parsers/smt2/smt2parser.cpp:2906
    #5 0x1b0bae0 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:3012
    #6 0x1b0cea1 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3141
    #7 0x1aebb0e in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3190
    #8 0x43ede7 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:142
    #9 0x466e50 in main ../src/shell/main.cpp:371
    #10 0x7f949ffa683f in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x2083f)
    #11 0x416118 in _start (/home/peisen/test/tofuzz/z3-debug/build/z3+0x416118)

AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV ../src/ast/ast.h:508 ast::get_kind() const

[NikolajBjorner]

first part is won't fix: "rem" is rewritten to mod, model validation is for uninterpreted version of mod, so it doesn't understand to use this for uninterpreted version of rem.