mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
minor code cleanup
This commit is contained in:
parent
3ebbb8472a
commit
59fa8964ca
|
@ -840,9 +840,8 @@ void bound_propagator::explain(var x, bound * b, unsigned ts, assumption_vector
|
|||
break;
|
||||
}
|
||||
}
|
||||
unsigned sz = todo.size();
|
||||
for (unsigned i = 0; i < sz; i++)
|
||||
todo[i].second->m_mark = false;
|
||||
for (var_bound& vb : todo)
|
||||
vb.second->m_mark = false;
|
||||
todo.reset();
|
||||
}
|
||||
|
||||
|
|
|
@ -135,9 +135,7 @@ struct propagate_ineqs_tactic::imp {
|
|||
mpq c_mpq_val;
|
||||
if (m_util.is_add(t)) {
|
||||
rational c_val;
|
||||
unsigned num = to_app(t)->get_num_args();
|
||||
for (unsigned i = 0; i < num; i++) {
|
||||
expr * mon = to_app(t)->get_arg(i);
|
||||
for (expr* mon : *to_app(t)) {
|
||||
expr * c, * x;
|
||||
if (m_util.is_mul(mon, c, x) && m_util.is_numeral(c, c_val)) {
|
||||
nm.set(c_mpq_val, c_val.to_mpq());
|
||||
|
|
|
@ -19,7 +19,6 @@ Notes:
|
|||
#include "tactic/tactical.h"
|
||||
#include "tactic/core/simplify_tactic.h"
|
||||
#include "tactic/core/propagate_values_tactic.h"
|
||||
#include "tactic/arith/propagate_ineqs_tactic.h"
|
||||
#include "tactic/core/solve_eqs_tactic.h"
|
||||
#include "tactic/core/elim_uncnstr_tactic.h"
|
||||
#include "tactic/smtlogics/smt_tactic.h"
|
||||
|
|
Loading…
Reference in a new issue