We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
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
[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
The text was updated successfully, but these errors were encountered:
93004a9
fix Z3Prover#4225
89bc160
No branches or pull requests
OS: Ubuntu 18.04
Commit: f2449df
The text was updated successfully, but these errors were encountered: