mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-21 11:52:05 +00:00
Code Activity

Yakir!

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-02-25 19:20:35 -08:00
parent d9b4f237fe
commit bef509b02e
1 changed files with 4 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/qe/qe_mbi.cpp
View file

@ -311,7 +311,7 @@ namespace qe {
//for (app* a : avars) shared.push_back(a->get_decl()); //for (app* a : avars) shared.push_back(a->get_decl());
tg.set_vars(shared, false); tg.set_vars(shared, false);
tg.add_lits(lits); tg.add_lits(lits);
//lits.reset(); lits.reset();
lits.append(tg.project(*mdl.get())); lits.append(tg.project(*mdl.get()));
TRACE("qe", tout << "project: " << lits << "\n";); TRACE("qe", tout << "project: " << lits << "\n";);
} }
@ -398,7 +398,9 @@ namespace qe {
// sort avars based on depth // sort avars based on depth
struct compare_depth { struct compare_depth {
bool operator()(app* x, app* y) const { bool operator()(app* x, app* y) const {
return x->get_depth() > y->get_depth(); return
(x->get_depth() > y->get_depth()) ||
(x->get_depth() == y->get_depth() && x->get_id() > y->get_id());
} }
}; };
compare_depth cmpd; compare_depth cmpd;