[622] % z3debug small.smt2
Segmentation fault
[623] % z3release small.smt2
Segmentation fault
[624] % z3san small.smt2
ASAN:DEADLYSIGNAL
=================================================================
==7796==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000008 (pc 0x55d5d8746f50 bp 0x7ffd196cb5d0 sp 0x7ffd196cb530 T0)
==7796==The signal is caused by a READ memory access.
==7796==Hint: address points to the zero page.
  #0 0x55d5d8746f4f in model::operator()(expr*) ../src/model/model.cpp:520
  #1 0x55d5d8746f4f in model::is_true(expr*) ../src/model/model.cpp:538
  #2 0x55d5d5f17d33 in spacer::context::handle_unknown(spacer::pob&, datalog::rule const*, model&) ../src/muz/spacer/spacer_context.cpp:3427
  #3 0x55d5d5f522ea in spacer::context::expand_pob(spacer::pob&, sref_buffer<spacer::pob, 16u>&) ../src/muz/spacer/spacer_context.cpp:3494
  #4 0x55d5d5f56272 in spacer::context::check_reachability() ../src/muz/spacer/spacer_context.cpp:3204
  #5 0x55d5d5f5e6de in spacer::context::solve_core(unsigned int) ../src/muz/spacer/spacer_context.cpp:3023
  #6 0x55d5d5f5f58c in spacer::context::solve(unsigned int) ../src/muz/spacer/spacer_context.cpp:2720
  #7 0x55d5d5ef7538 in spacer::dl_interface::query(expr*) ../src/muz/spacer/spacer_dl_interface.cpp:167
  #8 0x55d5d6724e9d in datalog::context::query(expr*) ../src/muz/base/dl_context.cpp:880
  #9 0x55d5d5e316ed in horn_tactic::imp::verify(expr*, ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&) ../src/muz/fp/horn_tactic.cpp:255
  #10 0x55d5d5e316ed in horn_tactic::imp::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/muz/fp/horn_tactic.cpp:241
  #11 0x55d5d86756f8 in cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:937
  #12 0x55d5d863fe4a in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:150
  #13 0x55d5d864214d in check_sat(tactic&, ref<goal>&, ref<model>&, labels_vec&, obj_ref<app, ast_manager>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >&) ../src/tactic/tactic.cpp:170
  #14 0x55d5d84ad9c8 in check_sat_core2 ../src/solver/tactic2solver.cpp:185
  #15 0x55d5d84ccb67 in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67
  #16 0x55d5d84e0394 in combined_solver::check_sat_core(unsigned int, expr* const*) ../src/solver/combined_solver.cpp:246
  #17 0x55d5d84bb761 in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:330
  #18 0x55d5d8436170 in cmd_context::check_sat(unsigned int, expr* const*) ../src/cmd_context/cmd_context.cpp:1549
  #19 0x55d5d83518b3 in smt2::parser::parse_check_sat() ../src/parsers/smt2/smt2parser.cpp:2595
  #20 0x55d5d83518b3 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2937
  #21 0x55d5d83518b3 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3129
  #22 0x55d5d8308e95 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3178
  #23 0x55d5d59b6ad6 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:90
  #24 0x55d5d596f2ee in main ../src/shell/main.cpp:352
  #25 0x7f98652d2b96 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21b96)
  #26 0x55d5d59835f9 in _start (/local/suz-local/software/z3san/build-05212020212726-18bb90f/z3+0x2135f9)
AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV ../src/model/model.cpp:520 in model::operator()(expr*)
==7796==ABORTING
[625] % 
[625] % cat small.smt2
(set-logic HORN)
(set-option :rlimit 610)
(set-option :rewriter.elim_and true)
(assert (forall ((a Int) (b Int)) (or (< a (mod b 2)) (forall ((c Int)) (> c b a)))))
(check-sat)
[626] %