[609] % z3san small.smt2
=================================================================
==15079==ERROR: AddressSanitizer: heap-use-after-free on address 0x6270000d6b30 at pc 0x55d07ee282fe bp 0x7ffcac018070 sp 0x7ffcac018060
READ of size 8 at 0x6270000d6b30 thread T0
  #0 0x55d07ee282fd in old_vector<unsigned int, false, unsigned int>::operator[](unsigned int) ../src/util/old_vector.h:371
  #1 0x55d07ee282fd in nla::emonics::remove_cg_mon(nla::monic const&) ../src/math/lp/emonics.cpp:205
  #2 0x55d07ee35e90 in nla::emonics::remove_cg(unsigned int) ../src/math/lp/emonics.cpp:187
  #3 0x55d07ee35e90 in nla::emonics::rehash_cg(unsigned int) ../src/math/lp/emonics.h:110
  #4 0x55d07ee35e90 in nla::emonics::after_merge_eh(nla::signed_var, nla::signed_var, nla::signed_var, nla::signed_var) ../src/math/lp/emonics.cpp:442
  #5 0x55d07ecdb6ff in nla::var_eqs<nla::emonics>::after_merge_eh(unsigned int, unsigned int, unsigned int, unsigned int) ../src/math/lp/var_eqs.h:347
  #6 0x55d07ecdb6ff in union_find<nla::var_eqs<nla::emonics> >::merge(unsigned int, unsigned int) ../src/util/union_find.h:134
  #7 0x55d07ecdc0e6 in nla::var_eqs<nla::emonics>::merge(nla::signed_var, nla::signed_var, nla::eq_justification const&) ../src/math/lp/var_eqs.h:121
  #8 0x55d07ecc213c in nla::var_eqs<nla::emonics>::merge_minus(unsigned int, unsigned int, nla::eq_justification const&) ../src/math/lp/var_eqs.h:129
  #9 0x55d07ecc213c in nla::core::add_equivalence_maybe(lp::lar_term const*, unsigned int, unsigned int) ../src/math/lp/nla_core.cpp:880
  #10 0x55d07ecc2d2e in nla::core::collect_equivs() ../src/math/lp/nla_core.cpp:840
  #11 0x55d07ecc3717 in nla::core::check(old_vector<nla::lemma, true, unsigned int>&) ../src/math/lp/nla_core.cpp:1497
  #12 0x55d07cf0bb32 in smt::theory_lra::imp::check_nra() ../src/smt/theory_lra.cpp:2237
  #13 0x55d07cf0bb32 in smt::theory_lra::imp::final_check_eh() ../src/smt/theory_lra.cpp:1741
  #14 0x55d07cf0bb32 in smt::theory_lra::final_check_eh() ../src/smt/theory_lra.cpp:3977
  #15 0x55d07ca6f8f4 in smt::context::final_check() ../src/smt/smt_context.cpp:3851
  #16 0x55d07ca7fd16 in smt::context::bounded_search() ../src/smt/smt_context.cpp:3767
  #17 0x55d07ca80617 in smt::context::search() ../src/smt/smt_context.cpp:3594
  #18 0x55d07ca8330d in smt::context::setup_and_check(bool) ../src/smt/smt_context.cpp:3417
  #19 0x55d07c90491f in smt_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/smt/tactic/smt_tactic.cpp:201
  #20 0x55d07e36a057 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
  #21 0x55d07e35c9b1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #22 0x55d07e35c9b1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #23 0x55d07e35c9b1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #24 0x55d07e35c9b1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #25 0x55d07e35c9b1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #26 0x55d07e35c9b1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #27 0x55d07e35c9b1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #28 0x55d07e35c9b1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #29 0x55d07e35c9b1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #30 0x55d07e35c9b1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #31 0x55d07e35c9b1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #32 0x55d07e35c9b1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #33 0x55d07e36a057 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
  #34 0x55d07e2cba4a in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:148
  #35 0x55d07e2cdd4d 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
  #36 0x55d07e1cc6a8 in check_sat_core2 ../src/solver/tactic2solver.cpp:185
  #37 0x55d07e1d3a67 in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67
  #38 0x55d07e191474 in combined_solver::check_sat_core(unsigned int, expr* const*) ../src/solver/combined_solver.cpp:246
  #39 0x55d07e172561 in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:330
  #40 0x55d07e0cd3b0 in cmd_context::check_sat(unsigned int, expr* const*) ../src/cmd_context/cmd_context.cpp:1551
  #41 0x55d07e014023 in smt2::parser::parse_check_sat() ../src/parsers/smt2/smt2parser.cpp:2596
  #42 0x55d07e014023 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2938
  #43 0x55d07e014023 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3130
  #44 0x55d07dfcb545 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3179
  #45 0x55d07b68a946 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:89
  #46 0x55d07b66341e in main ../src/shell/main.cpp:352
  #47 0x7f757421eb96 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21b96)
  #48 0x55d07b676fb9 in _start (/home/suz/software/z3san/build-04142020192323-164a73f/z3+0x1f6fb9)
...
SUMMARY: AddressSanitizer: heap-use-after-free ../src/util/old_vector.h:371 in old_vector<unsigned int, false, unsigned int>::operator[](unsigned int)
...
==15079==ABORTING
[610] % 
[610] % 
[610] % cat small.smt2
(set-option :rewriter.flat false)
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun aa () Real)
(declare-fun e () Real)
(declare-fun f () Real)
(declare-fun ab () Real)
(declare-fun ac () Real)
(declare-fun ad () Real)
(declare-fun g () Real)
(declare-fun h () Real)
(declare-fun i () Real)
(declare-fun j () Real)
(declare-fun k () Real)
(declare-fun l () Real)
(declare-fun m () Real)
(declare-fun n () Real)
(declare-fun o () Real)
(declare-fun v () Real)
(declare-fun ep () Real)
(declare-fun p () Real)
(declare-fun ae () Real)
(declare-fun q () Real)
(declare-fun r () Real)
(assert (forall ((af Real)) (=> (and (or (or (or (and (and (or (and
 (and (and (and (and (= o 0.0 (- aa)) (= (+ aa q) 2.0) ) (= (- e) 2.0)
 ) (>= 0 ac)) (= (/ 14 f ae) 2.0)) (<= o 0)) (< 0.0 (/ 14 b q))) (>
 0.0 a)) (< (* n) v(/ 5 d j))) (<= (* c (- 5 d)) v)) (<= 0.0 h)) (<
 0.0 v)) (>= 0.0 ep)) (or (= 0 ad) (<= 0.0 g) (<= af g) (or (or (or
 (<= 0.0 (/ 8 ab p)) (< p v)) (< 0.0 (/ (* h af) j))) (> (+ (+ h af)
 j) v)) (<= (- af) ep)) (= m 2.0))))
(assert (distinct c (* i ae)))
(assert (= aa (/ 78 k q)))
(assert (= e (* l q)))
(assert (= ab (/ v r)))
(check-sat)
[611] %