(rewriter.expand_nested_stores) Segmentation fault

[muchang]

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

[517] % z3release small.smt2
Segmentation fault
[518] % z3san small.smt2
ASAN:DEADLYSIGNAL
=================================================================
==57744==ERROR: AddressSanitizer: SEGV on unknown address 0x002e7fff8009 (pc 0x56397ef2ffbf bp 0x7ffe350733c0 sp 0x7ffe35073270 T0)
==57744==The signal is caused by a READ memory access.
  #0 0x56397ef2ffbe in smt::context::add_diseq(smt::enode*, smt::enode*) ../src/smt/smt_context.cpp:1060
  #1 0x56397ef4efa9 in smt::context::propagate_atoms() ../src/smt/smt_context.cpp:1326
  #2 0x56397ef5a895 in smt::context::propagate() ../src/smt/smt_context.cpp:1685
  #3 0x56397ef661a7 in smt::context::bounded_search() ../src/smt/smt_context.cpp:3725
  #4 0x56397ef66e07 in smt::context::search() ../src/smt/smt_context.cpp:3609
  #5 0x56397ef68e99 in smt::context::check(unsigned int, expr* const*, bool) ../src/smt/smt_context.cpp:3492
  #6 0x56397fb56219 in smt::model_checker::check(quantifier*) ../src/smt/smt_model_checker.cpp:356
  #7 0x56397fb56c01 in smt::model_checker::check_quantifiers(bool&, unsigned int&) ../src/smt/smt_model_checker.cpp:484
  #8 0x56397fb572ef in smt::model_checker::check(proto_model*, obj_map<smt::enode, app*> const&) ../src/smt/smt_model_checker.cpp:430
  #9 0x56397f680dc5 in smt::default_qm_plugin::check_model(proto_model*, obj_map<smt::enode, app*> const&) ../src/smt/smt_quantifier.cpp:722
  #10 0x56397f680dc5 in smt::quantifier_manager::imp::check_model(proto_model*, obj_map<smt::enode, app*> const&) ../src/smt/smt_quantifier.cpp:384
  #11 0x56397f680dc5 in smt::quantifier_manager::check_model(proto_model*, obj_map<smt::enode, app*> const&) ../src/smt/smt_quantifier.cpp:492
  #12 0x56397ef65166 in smt::context::restart(lbool&, unsigned int) ../src/smt/smt_context.cpp:3644
  #13 0x56397ef66e3e in smt::context::search() ../src/smt/smt_context.cpp:3614
  #14 0x56397ef69b3d in smt::context::setup_and_check(bool) ../src/smt/smt_context.cpp:3432
  #15 0x56397edecd2f in smt_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/smt/tactic/smt_tactic.cpp:201
  #16 0x56398088dd27 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
  #17 0x563980880791 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #18 0x563980880791 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #19 0x563980880791 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #20 0x563980880791 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #21 0x563980880791 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #22 0x563980880791 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #23 0x563980880791 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #24 0x563980880791 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #25 0x563980880791 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #26 0x563980880791 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #27 0x563980880791 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #28 0x563980880791 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #29 0x56398088dd27 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
  #30 0x5639807eff3a in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:148
  #31 0x5639807f223d 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:168
  #32 0x5639806f17c8 in check_sat_core2 ../src/solver/tactic2solver.cpp:185
  #33 0x5639806f8b87 in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67
  #34 0x5639806b64b4 in combined_solver::check_sat_core(unsigned int, expr* const*) ../src/solver/combined_solver.cpp:246
  #35 0x5639806974a1 in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:330
  #36 0x5639805e9e80 in cmd_context::check_sat(unsigned int, expr* const*) ../src/cmd_context/cmd_context.cpp:1549
  #37 0x563980539853 in smt2::parser::parse_check_sat() ../src/parsers/smt2/smt2parser.cpp:2596
  #38 0x563980539853 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2938
  #39 0x563980539853 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3130
  #40 0x5639804f0e45 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3179
  #41 0x56397db63646 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:89
  #42 0x56397db3bd0e in main ../src/shell/main.cpp:352
  #43 0x7fa3025d7b96 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21b96)
  #44 0x56397db4fc89 in _start (/home/suz/software/z3san/build-04292020120653-9f6a733/z3+0x211c89)
AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV ../src/smt/smt_context.cpp:1060 in smt::context::add_diseq(smt::enode*, smt::enode*)
==57744==ABORTING
[519] % 
[519] % cat small.smt2
(set-option :rewriter.expand_nested_stores true)
(declare-fun b ((Array Int (Array Int Real)) Int) Bool)
(declare-fun c () Int)
(declare-fun a0 () (Array Int (Array Int Real)))
(declare-fun d () Real)
(declare-fun a1 () (Array Int (Array Int Real)))
(declare-fun f () Real)
(declare-fun a3 () (Array Int (Array Int Real)))
(declare-fun e3 () Real)
(declare-fun a4 () (Array Int (Array Int Real)))
(declare-fun e4 () Real)
(declare-fun g () (Array Int (Array Int Real)))
(assert (forall ((a (Array Int (Array Int Real))) (c Int)) (distinct (b a c)
(exists ((h Int) (i Int)) (distinct (select (a h) i) (select (a i) h))))))
(assert (b a0 c))
(assert (= a1 (store a0 93 (store (select a0 0) (- 3) d)) (store a1 15 (store (select a1 204) 0 f))))
(assert (distinct a4 (store a3 0 (store (select a3 17) 0 e3)) (store a4 286 (store (select a4 4) 44 e4))))
(assert (b g c))
(check-sat)
[520] %

OS: Ubuntu 18.04
Commit: 9f6a733

[NikolajBjorner]

fixed