mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

merge

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-11-14 18:48:39 -08:00
parent ab4033133f 3a3e1796e2
commit 6ac95048e0
1 changed files with 6 additions and 6 deletions
Show stats 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);
}
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);
verbose_stream() << n->state() << "\n";);
}
}
else {
TRACE("pdr", tout << n->state() << "\n";);
}
else {
TRACE("pdr", tout << n->state() << "\n";);
}
todo.pop_back();
todo.append(n->children().size(), n->children().c_ptr());
}
@ -2037,11 +2037,11 @@ namespace pdr {
switch (expand_state(n, cube, uses_level)) {
case l_true:
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);
}
else {
TRACE("pdr", n.display(tout, 0););
TRACE("pdr", n.display(tout, 0););
create_children(n);
}
break;