[546] % z3 small.smt2
Segmentation fault
[547] % z3release small.smt2
Segmentation fault
[548] % z3san small.smt2
ASAN:DEADLYSIGNAL
=================================================================
==3865==ERROR: AddressSanitizer: stack-overflow on address 0x7fff63db7f78 (pc 0x7fafca104b67 bp 0x7fff63db87e0 sp 0x7fff63db7f50 T0)
  #0 0x7fafca104b66 in __interceptor_memmove (/usr/lib/x86_64-linux-gnu/libasan.so.4+0x7ab66)
  #1 0x55b75635ccfa in expr** std::__copy_move_backward<true, true, std::random_access_iterator_tag>::__copy_move_b<expr*>(expr* const*, expr* const*, expr**) /usr/include/c++/7/bits/stl_algobase.h:570
  #2 0x55b75635ccfa in expr** std::__copy_move_backward_a<true, expr**, expr**>(expr**, expr**, expr**) /usr/include/c++/7/bits/stl_algobase.h:590
  #3 0x55b75635ccfa in expr** std::__copy_move_backward_a2<true, expr**, expr**>(expr**, expr**, expr**) /usr/include/c++/7/bits/stl_algobase.h:599
  #4 0x55b75635ccfa in expr** std::move_backward<expr**, expr**>(expr**, expr**, expr**) /usr/include/c++/7/bits/stl_algobase.h:670
  #5 0x55b75635ccfa in void std::__insertion_sort<expr**, __gnu_cxx::__ops::_Iter_comp_iter<poly_rewriter<arith_rewriter_core>::mon_lt> >(expr**, expr**, __gnu_cxx::__ops::_Iter_comp_iter<poly_rewriter<arith_rewriter_core>::mon_lt>) /usr/include/c++/7/bits/stl_algo.h:1851
  #6 0x55b75635ccfa in void std::__final_insertion_sort<expr**, __gnu_cxx::__ops::_Iter_comp_iter<poly_rewriter<arith_rewriter_core>::mon_lt> >(expr**, expr**, __gnu_cxx::__ops::_Iter_comp_iter<poly_rewriter<arith_rewriter_core>::mon_lt>) /usr/include/c++/7/bits/stl_algo.h:1890
  #7 0x55b75635ccfa in void std::__sort<expr**, __gnu_cxx::__ops::_Iter_comp_iter<poly_rewriter<arith_rewriter_core>::mon_lt> >(expr**, expr**, __gnu_cxx::__ops::_Iter_comp_iter<poly_rewriter<arith_rewriter_core>::mon_lt>) /usr/include/c++/7/bits/stl_algo.h:1971
  #8 0x55b756363799 in void std::sort<expr**, poly_rewriter<arith_rewriter_core>::mon_lt>(expr**, expr**, poly_rewriter<arith_rewriter_core>::mon_lt) /usr/include/c++/7/bits/stl_algo.h:4868
  #9 0x55b756363799 in poly_rewriter<arith_rewriter_core>::mk_nflat_add_core(unsigned int, expr* const*, obj_ref<expr, ast_manager>&) ../src/ast/rewriter/poly_rewriter_def.h:615
  #10 0x55b7563668f4 in poly_rewriter<arith_rewriter_core>::mk_flat_add_core(unsigned int, expr* const*, obj_ref<expr, ast_manager>&) ../src/ast/rewriter/poly_rewriter_def.h:426
  #11 0x55b756344bd4 in poly_rewriter<arith_rewriter_core>::mk_add_core(unsigned int, expr* const*, obj_ref<expr, ast_manager>&) ../src/ast/rewriter/poly_rewriter.h:147
  #12 0x55b756344bd4 in arith_rewriter::mk_add_core(unsigned int, expr* const*, obj_ref<expr, ast_manager>&) ../src/ast/rewriter/arith_rewriter.cpp:657
  #13 0x55b756078e1b in reduce_app_core ../src/ast/rewriter/th_rewriter.cpp:207
  #14 0x55b756078e1b in reduce_app ../src/ast/rewriter/th_rewriter.cpp:616
  #15 0x55b7560837fa in process_app<false> ../src/ast/rewriter/rewriter_def.h:299
  #16 0x55b7560837fa in resume_core<false> ../src/ast/rewriter/rewriter_def.h:770
  #17 0x55b7560925da in main_loop<false> ../src/ast/rewriter/rewriter_def.h:729
  #18 0x55b7560925da in operator() ../src/ast/rewriter/rewriter_def.h:801
  #19 0x55b7560925da in th_rewriter::operator()(expr*, obj_ref<expr, ast_manager>&, obj_ref<app, ast_manager>&) ../src/ast/rewriter/th_rewriter.cpp:855
  #20 0x55b7559f2f20 in simplify_tactic::imp::operator()(goal&) ../src/tactic/core/simplify_tactic.cpp:57
  #21 0x55b7559f2f20 in simplify_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/core/simplify_tactic.cpp:94
  #22 0x55b755e36168 in cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:915
  #23 0x55b755e41c50 in repeat_tactical::operator()(unsigned int, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:811
  #24 0x55b755e42ec1 in repeat_tactical::operator()(unsigned int, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:825
  #25 0x55b755e42ec1 in repeat_tactical::operator()(unsigned int, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:825
  #26 0x55b755e42ec1 in repeat_tactical::operator()(unsigned int, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:825
...
SUMMARY: AddressSanitizer: stack-overflow (/usr/lib/x86_64-linux-gnu/libasan.so.4+0x7ab66) in __interceptor_memmove
==3865==ABORTING
[549] % 
[549] % cat small.smt2
(set-option :rewriter.arith_lhs true)
(set-option :rewriter.sort_sums true)
(assert (forall ((a Int) (b Int)) (= b (ite (= a 1) 10 0))))
(apply (repeat simplify))
[550] %