Skip to content

Segfault on trivial formula #4225

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
wintered opened this issue May 6, 2020 · 0 comments
Closed

Segfault on trivial formula #4225

wintered opened this issue May 6, 2020 · 0 comments

Comments

@wintered
Copy link

wintered commented May 6, 2020

[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] %

OS: Ubuntu 18.04
Commit: f2449df

hgvk94 pushed a commit to hgvk94/z3 that referenced this issue May 7, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant