mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
rmove debug out
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
886d3f4351
commit
421fe94607
|
@ -1529,12 +1529,10 @@ public:
|
|||
unsigned old_sz = m_assume_eq_candidates.size();
|
||||
unsigned num_candidates = 0;
|
||||
int start = ctx().get_random_value();
|
||||
verbose_stream() << "assume-eqs " << sz << "\n";
|
||||
unsigned num_relevant = 0;
|
||||
for (theory_var i = 0; i < sz; ++i) {
|
||||
theory_var v = (i + start) % sz;
|
||||
enode* n1 = get_enode(v);
|
||||
verbose_stream() << enode_pp(n1, ctx()) << "\n";
|
||||
if (!th.is_relevant_and_shared(n1)) {
|
||||
continue;
|
||||
}
|
||||
|
@ -1557,7 +1555,6 @@ public:
|
|||
}
|
||||
}
|
||||
|
||||
verbose_stream() << "candidates " << num_candidates << " num relevant " << num_relevant << "\n";
|
||||
if (num_candidates > 0) {
|
||||
ctx().push_trail(restore_vector(m_assume_eq_candidates, old_sz));
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue