mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-18 10:30:44 +00:00
Code Activity

Fix issue #311

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

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

@ -929,7 +929,7 @@ namespace pdr {
model_node* p = n.parent(); model_node* p = n.parent();
while (p) { while (p) {
if (p->state() == n.state()) { if (p->state() == n.state()) {
TRACE("pdr", tout << "repeated\n";); TRACE("pdr", tout << n.state() << "repeated\n";);
return true; return true;
} }
p = p->parent(); p = p->parent();
@ -1019,6 +1019,11 @@ namespace pdr {
SASSERT(n1->children().empty()); SASSERT(n1->children().empty());
enqueue_leaf(n1); enqueue_leaf(n1);
} }
if (!nodes.empty() && n.get_model_ptr() && backtrack) {
model_ref mr(n.get_model_ptr());
nodes[0]->set_model(mr);
}
if (nodes.empty()) { if (nodes.empty()) {
cache(n).remove(n.state()); cache(n).remove(n.state());
} }