(model_validate, ufbv) Segmentation fault on QF_UFLIA

[muchang]

Hi,
For this case, Z3 throws out a segmentation fault:

[612] % z3debug model_validate=true small.smt2
sat
Segmentation fault
[613] % z3release model_validate=true small.smt2
sat
Segmentation fault
[614] % z3san model_validate=true small.smt2
sat
ASAN:DEADLYSIGNAL
=================================================================
==10551==ERROR: AddressSanitizer: stack-overflow on address 0x7fff86460ff8 (pc 0x7fec5715ebf4 bp 0x7fff86461870 sp 0x7fff86461000 T0)
  #0 0x7fec5715ebf3 (/usr/lib/x86_64-linux-gnu/libasan.so.4+0xeebf3)
  #1 0x7fec5714eb67 in __interceptor_malloc (/usr/lib/x86_64-linux-gnu/libasan.so.4+0xdeb67)
  #2 0x55fe46d4537d in memory::allocate(unsigned long) ../src/util/memory_manager.cpp:268
  #3 0x55fe45a838ce in rewriter_core::init_cache_stack() ../src/ast/rewriter/rewriter.cpp:26
  #4 0x55fe45a838ce in rewriter_core::rewriter_core(ast_manager&, bool) ../src/ast/rewriter/rewriter.cpp:196
  #5 0x55fe4559a7c0 in rewriter_tpl<mev::evaluator_cfg>::rewriter_tpl(ast_manager&, bool, mev::evaluator_cfg&) ../src/ast/rewriter/rewriter_def.h:623
  #6 0x55fe4559a7c0 in model_evaluator::imp::imp(model_core&, params_ref const&) ../src/model/model_evaluator.cpp:602
  #7 0x55fe455ad8e6 in model_evaluator::model_evaluator(model_core&, params_ref const&) ../src/model/model_evaluator.cpp:614
  #8 0x55fe455ad8e6 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
  #9 0x55fe455b60c4 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
  #10 0x55fe455b60c4 in bool rewriter_tpl<mev::evaluator_cfg>::process_const<false>(app*) ../src/ast/rewriter/rewriter_def.h:82
  #11 0x55fe455b6835 in bool rewriter_tpl<mev::evaluator_cfg>::visit<false>(expr*, unsigned int) ../src/ast/rewriter/rewriter_def.h:190
  #12 0x55fe455a90f4 in void rewriter_tpl<mev::evaluator_cfg>::process_app<false>(app*, rewriter_core::frame&) ../src/ast/rewriter/rewriter_def.h:260
  #13 0x55fe455aa9fd 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
  #14 0x55fe455ab861 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
  #15 0x55fe455930bb 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
  #16 0x55fe455930bb in rewriter_tpl<mev::evaluator_cfg>::operator()(expr*, obj_ref<expr, ast_manager>&) ../src/ast/rewriter/rewriter.h:357
  #17 0x55fe455930bb in model_evaluator::operator()(expr*, obj_ref<expr, ast_manager>&) ../src/model/model_evaluator.cpp:671
  #18 0x55fe455930bb in model_evaluator::operator()(expr*) ../src/model/model_evaluator.cpp:679
...
SUMMARY: AddressSanitizer: stack-overflow (/usr/lib/x86_64-linux-gnu/libasan.so.4+0xeebf3) 
==10551==ABORTING
[615] % 
[615] % cat small.smt2
(declare-fun a (Int) Bool)
(declare-fun b (Int) Bool)
(assert (= (= a b) (b 0)))
(check-sat-using ufbv)
[616] %

OS: Ubuntu 18.04
Commit: 6a540e8