[503] % z3 small.smt2
unsat
ASSERTION VIOLATION
File: ../src/nlsat/nlsat_solver.cpp
Line: 950
num_lits > 0
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[504] % z3release small.smt2
unsat
Segmentation fault
[505] % z3san small.smt2
unsat
ASAN:DEADLYSIGNAL
=================================================================
==18154==ERROR: AddressSanitizer: SEGV on unknown address 0x603400044328 (pc 0x55c59dfdb87e bp 0x7ffd2f126c00 sp 0x7ffd2f126bf0 T0)
==18154==The signal is caused by a READ memory access.
  #0 0x55c59dfdb87d in vector<nlsat::clause*, false, unsigned int>::push_back(nlsat::clause*&&) ../src/util/vector.h:434
  #1 0x55c59dfdbc35 in nlsat::solver::imp::attach_clause(nlsat::clause&) ../src/nlsat/nlsat_solver.cpp:703
  #2 0x55c59dfef399 in nlsat::solver::imp::mk_clause(unsigned int, sat::literal const*, bool, dependency_manager<nlsat::solver::imp::dconfig>::dependency*) ../src/nlsat/nlsat_solver.cpp:945
  #3 0x55c59cb766f4 in goal2nlsat::imp::process(expr*, dependency_manager<ast_manager::expr_dependency_config>::dependency*) ../src/nlsat/tactic/goal2nlsat.cpp:251
  #4 0x55c59cb766f4 in goal2nlsat::imp::operator()(goal const&) ../src/nlsat/tactic/goal2nlsat.cpp:260
  #5 0x55c59cb766f4 in goal2nlsat::operator()(goal const&, params_ref const&, nlsat::solver&, expr2var&, expr2var&) ../src/nlsat/tactic/goal2nlsat.cpp:294
  #6 0x55c59cb71cc4 in nlsat_tactic::imp::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/nlsat/tactic/nlsat_tactic.cpp:149
  #7 0x55c59cb745e6 in nlsat_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/nlsat/tactic/nlsat_tactic.cpp:241
  #8 0x55c59d4311c8 in cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:918
  #9 0x55c59d3fb91a in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:150
  #10 0x55c59d3fdc1d 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
  #11 0x55c59d173320 in check_sat_using_tactict_cmd::execute(cmd_context&) ../src/cmd_context/tactic_cmds.cpp:223
  #12 0x55c59d1062e8 in smt2::parser::parse_ext_cmd(int, int) ../src/parsers/smt2/smt2parser.cpp:2895
  #13 0x55c59d10d33c in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:3001
  #14 0x55c59d10d33c in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3130
  #15 0x55c59d0c4aa5 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3179  
  #16 0x55c59a755c26 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:89
  #17 0x55c59a70e3ae in main ../src/shell/main.cpp:352
  #18 0x7ff8a7527b96 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21b96)
  #19 0x55c59a7225f9 in _start (/local/suz-local/software/z3san/build-05052020155909-f2449df/z3+0x2125f9)
AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV ../src/util/vector.h:434 in vector<nlsat::clause*, false, unsigned int>::push_back(nlsat::clause*&&)
==18154==ABORTING
[506] %
[506] % cat small.smt2
(assert or)
(check-sat)
(check-sat-using nlsat)
[507] %