mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-21 13:23:39 +00:00
Code Activity

Fix bug #311. update tabs

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-11-14 18:42:11 -08:00
parent f537167080
commit 3a3e1796e2
1 changed files with 6 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/muz/pdr/pdr_context.cpp
View file

@ -1162,14 +1162,14 @@ namespace pdr {
n->set_rule(rule); n->set_rule(rule);
} }
else { else {
TRACE("pdr", tout << "no model for " << n->state() << "\n";); TRACE("pdr", tout << "no model for " << n->state() << "\n";);
IF_VERBOSE(1, n->display(verbose_stream() << "no model:\n", 0); IF_VERBOSE(1, n->display(verbose_stream() << "no model:\n", 0);
verbose_stream() << n->state() << "\n";); verbose_stream() << n->state() << "\n";);
} }
} }
else { else {
TRACE("pdr", tout << n->state() << "\n";); TRACE("pdr", tout << n->state() << "\n";);
} }
todo.pop_back(); todo.pop_back();
todo.append(n->children().size(), n->children().c_ptr()); todo.append(n->children().size(), n->children().c_ptr());
} }
@ -2037,11 +2037,11 @@ namespace pdr {
switch (expand_state(n, cube, uses_level)) { switch (expand_state(n, cube, uses_level)) {
case l_true: case l_true:
if (n.level() == 0) { if (n.level() == 0) {
TRACE("pdr", n.display(tout << "reachable at level 0\n", 0);); TRACE("pdr", n.display(tout << "reachable at level 0\n", 0););
close_node(n); close_node(n);
} }
else { else {
TRACE("pdr", n.display(tout, 0);); TRACE("pdr", n.display(tout, 0););
create_children(n); create_children(n);
} }
break; break;