mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

make bpp work with nullptr

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-07-12 00:03:32 +02:00
parent 4c53655be7
commit de8b2041e6
2 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/ast/ast_ll_pp.cpp
View file

@ -303,7 +303,9 @@ public:
} }
void display_bounded(ast * n, unsigned depth) { void display_bounded(ast * n, unsigned depth) {
if (is_app(n)) { if (!n)
m_out << "null";
else if (is_app(n)) {
display(to_expr(n), depth); display(to_expr(n), depth);
} }
else if (is_var(n)) { else if (is_var(n)) {

6
src/sat/smt/euf_solver.cpp
View file

@ -286,11 +286,9 @@ namespace euf {
void solver::asserted(literal l) { void solver::asserted(literal l) {
expr* e = m_bool_var2expr.get(l.var(), nullptr); expr* e = m_bool_var2expr.get(l.var(), nullptr);
if (!e) { TRACE("euf", tout << "asserted: " << l << "@" << s().scope_lvl() << " := " << mk_bounded_pp(e, m) << "\n";);
TRACE("euf", tout << "asserted: " << l << "@" << s().scope_lvl() << "\n";); if (!e)
return; return;
}
TRACE("euf", tout << "asserted: " << l << "@" << s().scope_lvl() << " := " << mk_bounded_pp(e, m) << "\n";);
euf::enode* n = m_egraph.find(e); euf::enode* n = m_egraph.find(e);
if (!n) if (!n)
return; return;