mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 05:18:44 +00:00
Code Activity

fix 'make test' for newer gcc versions

Browse source 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
This commit is contained in:
Nuno Lopes 2015-05-19 13:48:14 +01:00
parent 8ff7735a20
commit 4c7fea7e55
1 changed files with 9 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/test/pdr.cpp
View file

@ -47,10 +47,15 @@ struct test_model_search {
void add_tree(model_node* parent, bool force_goal) {
unsigned level = parent->level();
search.add_leaf(*parent);
expr_ref state(m);
if (level > 0 && (force_goal || parent->is_goal())) {
search.remove_goal(*parent);
add_tree(alloc(model_node, parent, mk_state(states, rand), pt, level-1), false);
add_tree(alloc(model_node, parent, mk_state(states, rand), pt, level-1), false);
state = mk_state(states, rand);
add_tree(alloc(model_node, parent, state, pt, level-1), false);
state = mk_state(states, rand);
add_tree(alloc(model_node, parent, state, pt, level-1), false);
parent->check_pre_closed();
}
}
@ -91,7 +96,8 @@ struct test_model_search {
state = states[0].get();
unsigned level = 4;
for(unsigned n = 0; n < 100; ++n) {
model_node* root = alloc(model_node, 0, mk_state(states, rand), pt, level);
state = mk_state(states, rand);
model_node* root = alloc(model_node, 0, state, pt, level);
search.set_root(root);
add_tree(root, false);
search.display(std::cout);