mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity

use usize to suppress the data loss warnings

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-07-02 14:42:55 -07:00
parent f544dd4ab2
commit d2990e2f68
2 changed files with 4 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/nlsat/nlsat_simplify.cpp
View file

@ -66,7 +66,7 @@ namespace nlsat {
polynomial_ref p(m_pm);
ptr_buffer<poly> ps;
buffer<bool> is_even;
unsigned num_atoms = m_atoms.size();
unsigned num_atoms = usize(m_atoms);
for (unsigned j = 0; j < num_atoms; ++j) {
atom* a1 = m_atoms[j];
if (a1 && a1->is_ineq_atom()) {

6
src/nlsat/nlsat_solver.cpp
View file

@ -2616,7 +2616,7 @@ namespace nlsat {
bool check_satisfied() {
TRACE(nlsat, tout << "bk: b" << m_bk << ", xk: x" << m_xk << "\n"; if (m_xk != null_var) { m_display_var(tout, m_xk); tout << "\n"; });
unsigned num = m_atoms.size();
unsigned num = usize(m_atoms);
if (m_bk != null_bool_var)
num = m_bk;
for (bool_var b = 0; b < num; b++) {
@ -3273,7 +3273,7 @@ namespace nlsat {
}
std::ostream& display_bool_assignment(std::ostream & out, bool eval_atoms = false) const {
unsigned sz = m_atoms.size();
unsigned sz = usize(m_atoms);
if (!eval_atoms) {
for (bool_var b = 0; b < sz; b++) {
if (m_bvalues[b] == l_undef)
@ -4011,7 +4011,7 @@ namespace nlsat {
}
std::ostream& display_smt2_bool_decls(std::ostream & out) const {
unsigned sz = m_atoms.size();
unsigned sz = usize(m_atoms);
for (unsigned i = 0; i < sz; i++) {
if (m_atoms[i] == nullptr)
out << "(declare-fun b" << i << " () Bool)\n";