[601] % z3debug small.smt2
unknown
[602] % z3debug model_validate=true parallel.enable=true small.smt2
sat
Segmentation fault
[603] % z3release model_validate=true parallel.enable=true small.smt2
sat
Segmentation fault
[604] % z3san model_validate=true parallel.enable=true small.smt2
sat
ASAN:DEADLYSIGNAL
=================================================================
==3162==ERROR: AddressSanitizer: stack-overflow on address 0x7fff04698fe8 (pc 0x7f803d4ceade bp 0x7fff04699850 sp 0x7fff04698ff0 T0)
  #0 0x7f803d4ceadd in __interceptor_malloc (/usr/lib/x86_64-linux-gnu/libasan.so.4+0xdeadd)
  #1 0x5593ce6e52dd in memory::allocate(unsigned long) ../src/util/memory_manager.cpp:268
  #2 0x5593cd42334e in rewriter_core::init_cache_stack() ../src/ast/rewriter/rewriter.cpp:26
  #3 0x5593cd42334e in rewriter_core::rewriter_core(ast_manager&, bool) ../src/ast/rewriter/rewriter.cpp:196
  #4 0x5593ccf39690 in rewriter_tpl<mev::evaluator_cfg>::rewriter_tpl(ast_manager&, bool, mev::evaluator_cfg&) ../src/ast/rewriter/rewriter_def.h:623
  #5 0x5593ccf39690 in model_evaluator::imp::imp(model_core&, params_ref const&) ../src/model/model_evaluator.cpp:602
  #6 0x5593ccf4c7b6 in model_evaluator::model_evaluator(model_core&, params_ref const&) ../src/model/model_evaluator.cpp:614
  #7 0x5593ccf4c7b6 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:257
  #8 0x5593ccf54f94 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:148
  #9 0x5593ccf54f94 in bool rewriter_tpl<mev::evaluator_cfg>::process_const<false>(app*) ../src/ast/rewriter/rewriter_def.h:82
  #10 0x5593ccf55705 in bool rewriter_tpl<mev::evaluator_cfg>::visit<false>(expr*, unsigned int) ../src/ast/rewriter/rewriter_def.h:190
  #11 0x5593ccf47fc4 in void rewriter_tpl<mev::evaluator_cfg>::process_app<false>(app*, rewriter_core::frame&) ../src/ast/rewriter/rewriter_def.h:260
  #12 0x5593ccf498cd 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:769
  #13 0x5593ccf4a731 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:728
  #14 0x5593ccf31f8b in rewriter_tpl<mev::evaluator_cfg>::operator()(expr*, obj_ref<expr, ast_manager>&, obj_ref<app, ast_manager>&) ../src/ast/rewriter/rewriter_def.h:800
  #15 0x5593ccf31f8b in rewriter_tpl<mev::evaluator_cfg>::operator()(expr*, obj_ref<expr, ast_manager>&) ../src/ast/rewriter/rewriter.h:357
  #16 0x5593ccf31f8b in model_evaluator::operator()(expr*, obj_ref<expr, ast_manager>&) ../src/model/model_evaluator.cpp:671
  #17 0x5593ccf31f8b in model_evaluator::operator()(expr*) ../src/model/model_evaluator.cpp:679
  #18 0x5593ccf4c81d 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:258
  #19 0x5593ccf54f94 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:148
  #20 0x5593ccf54f94 in bool rewriter_tpl<mev::evaluator_cfg>::process_const<false>(app*) ../src/ast/rewriter/rewriter_def.h:82
  #21 0x5593ccf55705 in bool rewriter_tpl<mev::evaluator_cfg>::visit<false>(expr*, unsigned int) ../src/ast/rewriter/rewriter_def.h:190
  #22 0x5593ccf47fc4 in void rewriter_tpl<mev::evaluator_cfg>::process_app<false>(app*, rewriter_core::frame&) ../src/ast/rewriter/rewriter_def.h:260
  #23 0x5593ccf498cd 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:769
...
SUMMARY: AddressSanitizer: stack-overflow (/usr/lib/x86_64-linux-gnu/libasan.so.4+0xdeadd) in __interceptor_malloc
==3162==ABORTING
[605] % 
[605] % cat small.smt2
(declare-fun a (Int) Bool)
(declare-fun b (Int) Bool)
(assert (xor (= a b) (b 0)))
(check-sat-using (then qfbv default))
[606] %