Assertion violation at src/util/vector.h:73

[wintered]

[638] % z3 small.smt2
sat
sat
ASSERTION VIOLATION
File: ../src/util/vector.h
Line: 73
capacity() > 0
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[639] % 
[639] % z3release small.smt2
sat
sat
Segmentation fault
[640] % 
[640] % z3san small.smt2
sat
sat
=================================================================
==19402==ERROR: AddressSanitizer: heap-use-after-free on address 0x616000000590 at pc 0x55b1d691eb52 bp 0x7ffc8043a400 sp 0x7ffc8043a3f0
READ of size 8 at 0x616000000590 thread T0
  #0 0x55b1d691eb51 in old_vector<sexpr*, false, unsigned int>::push_back(sexpr* const&) ../src/util/old_vector.h:418
  #1 0x55b1d691eb51 in sexpr_manager::del(sexpr*) ../src/util/sexpr.cpp:218
  #2 0x55b1d4e3ce37 in sexpr_manager::dec_ref(sexpr*) ../src/util/sexpr.h:78
  #3 0x55b1d4e3ce37 in ref_manager_wrapper<sexpr, sexpr_manager>::dec_ref(sexpr*) ../src/util/ref_vector.h:199
  #4 0x55b1d4e3ce37 in ref_vector_core<sexpr, ref_manager_wrapper<sexpr, sexpr_manager> >::dec_ref(sexpr*) ../src/util/ref_vector.h:37
  #5 0x55b1d4e3ce37 in ref_vector_core<sexpr, ref_manager_wrapper<sexpr, sexpr_manager> >::dec_range_ref(sexpr* const*, sexpr* const*) ../src/util/ref_vector.h:41
  #6 0x55b1d4e3ce37 in ref_vector_core<sexpr, ref_manager_wrapper<sexpr, sexpr_manager> >::shrink(unsigned int) ../src/util/ref_vector.h:92
  #7 0x55b1d4e3ce37 in void smt2::parser::shrink<ref_vector<sexpr, sexpr_manager> >(scoped_ptr<ref_vector<sexpr, sexpr_manager> >&, unsigned int) ../src/parsers/smt2/smt2parser.cpp:257
  #8 0x55b1d4e3ce37 in smt2::parser::parse_ext_cmd(int, int) ../src/parsers/smt2/smt2parser.cpp:2900
  #9 0x55b1d4e4407c in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:3001
  #10 0x55b1d4e4407c in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3130
  #11 0x55b1d4dfb715 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3179
  #12 0x55b1d24b9c86 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:89
  #13 0x55b1d249275e in main ../src/shell/main.cpp:352
  #14 0x7fd7d17afb96 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21b96)
  #15 0x55b1d24a62f9 in _start (/home/suz/software/z3san/build-04152020103633-068f65c/z3+0x1f72f9)
...
==19402==ABORTING
[641] % 
[641] % 
[641] % cat small.smt2
(set-option :trace true)
(check-sat-using default)
(reset-assertions)
(declare-fun a () Int)
(check-sat-using default)
[642] %

OS: Ubuntu 18.04 Commit: dde0c51

[NikolajBjorner]

fixed