[519] % z3release small.smt2
Segmentation fault
[520] % z3debug small.smt2
Segmentation fault
[521] % z3san small.smt2
ASAN:DEADLYSIGNAL
=================================================================
==20593==ERROR: AddressSanitizer: stack-overflow on address 0x7ffd3259cfc0 (pc 0x55c5658b71e6 bp 0x7ffd3259d040 sp 0x7ffd3259cfb0 T0)
    #0 0x55c5658b71e5 in ast_manager::get_plugin(int) const ../src/ast/ast.cpp:1634
    #1 0x55c565663c73 in arith_util::init_plugin() ../src/ast/arith_decl_plugin.cpp:749
    #2 0x55c565663c73 in arith_util::plugin() const ../src/ast/arith_decl_plugin.h:374
    #3 0x55c565663c73 in arith_util::is_considered_uninterpreted(func_decl*, unsigned int, expr* const*, obj_ref<func_decl, ast_manager>&) ../src/ast/arith_decl_plugin.cpp:831
    #4 0x55c5645a3ecf in mev::evaluator_cfg::evaluate_partial_theory_func(func_decl*, unsigned int, expr* const*, obj_ref<expr, ast_manager>&, obj_ref<app, ast_manager>&) ../src/model/model_evaluator.cpp:352
    #5 0x55c5645ab361 in mev::evaluator_cfg::reduce_app_core(func_decl*, unsigned int, expr* const*, obj_ref<expr, ast_manager>&, obj_ref<app, ast_manager>&) ../src/model/model_evaluator.cpp:249
    #6 0x55c5645b3c34 in mev::evaluator_cfg::reduce_app(func_decl*, unsigned int, expr* const*, obj_ref<expr, ast_manager>&, obj_ref<app, ast_manager>&) ../src/model/model_evaluator.cpp:150
    #7 0x55c5645b3c34 in bool rewriter_tpl<mev::evaluator_cfg>::process_const<false>(app*) ../src/ast/rewriter/rewriter_def.h:83
    #8 0x55c5645b43a5 in bool rewriter_tpl<mev::evaluator_cfg>::visit<false>(expr*, unsigned int) ../src/ast/rewriter/rewriter_def.h:195
    #9 0x55c5645a67e4 in void rewriter_tpl<mev::evaluator_cfg>::process_app<false>(app*, rewriter_core::frame&) ../src/ast/rewriter/rewriter_def.h:265
    #10 0x55c5645a881d in void rewriter_tpl<mev::evaluator_cfg>::resume_core<false>(obj_ref<expr, ast_manager>&, obj_ref<app, ast_manager>&) ../src/ast/rewriter/rewriter_def.h:774
    #11 0x55c5645a9701 in void rewriter_tpl<mev::evaluator_cfg>::main_loop<false>(expr*, obj_ref<expr, ast_manager>&, obj_ref<app, ast_manager>&) ../src/ast/rewriter/rewriter_def.h:733
    #12 0x55c56459205b in rewriter_tpl<mev::evaluator_cfg>::operator()(expr*, obj_ref<expr, ast_manager>&, obj_ref<app, ast_manager>&) ../src/ast/rewriter/rewriter_def.h:813
    #13 0x55c56459205b in rewriter_tpl<mev::evaluator_cfg>::operator()(expr*, obj_ref<expr, ast_manager>&) ../src/ast/rewriter/rewriter.h:356
    #14 0x55c56459205b in model_evaluator::operator()(expr*, obj_ref<expr, ast_manager>&) ../src/model/model_evaluator.cpp:686
    #15 0x55c564593481 in model_evaluator::operator()(expr*) ../src/model/model_evaluator.cpp:694
    #16 0x55c5645ab0dc in mev::evaluator_cfg::reduce_app_core(func_decl*, unsigned int, expr* const*, obj_ref<expr, ast_manager>&, obj_ref<app, ast_manager>&) ../src/model/model_evaluator.cpp:269
    #17 0x55c5645b3c34 in mev::evaluator_cfg::reduce_app(func_decl*, unsigned int, expr* const*, obj_ref<expr, ast_manager>&, obj_ref<app, ast_manager>&) ../src/model/model_evaluator.cpp:150
    #18 0x55c5645b3c34 in bool rewriter_tpl<mev::evaluator_cfg>::process_const<false>(app*) ../src/ast/rewriter/rewriter_def.h:83
...
SUMMARY: AddressSanitizer: stack-overflow ../src/ast/ast.cpp:1634 in ast_manager::get_plugin(int) const
==20593==ABORTING
[522] % 
[522] % cat small.smt2
(set-option :model_evaluator.completion true)
(set-option :rewriter.expand_nested_stores true)
(declare-fun a () (Array (_ BitVec 2) (_ BitVec 2)))
(declare-fun b () (Array (_ BitVec 2) (_ BitVec 2)))
(declare-fun c () (Array (_ BitVec 2) (_ BitVec 2)))
(assert
 (= (_ bv1 1)
  (bvsdiv (_ bv1 1)
   (bvand
    (ite (= a (store (store (store b (_ bv0 2) (_ bv0 2)) (_ bv1 2) (_ bv1 2)) (_ bv0 2) (_ bv0 2)))
     (_ bv1 1)
     (_ bv0 1))
    (bvcomp (_ bv0 1)
     (ite (= a (store (store (store c (_ bv1 2) (_ bv1 2)) (_ bv0 2) (_ bv1 2)) (_ bv1 2) (_ bv0 2)))
      (_ bv1 1)
      (_ bv0 1)))))))
(check-sat)
[523] %