mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-22 22:03:39 +00:00
Code Activity

fix some build warnings exposed in #5005

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-02-08 10:57:43 -08:00
parent 8fffc03263
commit b56372fe76
3 changed files with 4 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/nlsat/nlsat_explain.cpp
View file

@ -907,9 +907,9 @@ namespace nlsat {
TRACE("nlsat_explain", tout << "adding literals for "; display_var(tout, y); tout << " -> "; TRACE("nlsat_explain", tout << "adding literals for "; display_var(tout, y); tout << " -> ";
m_am.display_decimal(tout, y_val); tout << "\n";); m_am.display_decimal(tout, y_val); tout << "\n";);
polynomial_ref p_lower(m_pm); polynomial_ref p_lower(m_pm);
unsigned i_lower; unsigned i_lower = UINT_MAX;
polynomial_ref p_upper(m_pm); polynomial_ref p_upper(m_pm);
unsigned i_upper; unsigned i_upper = UINT_MAX;
polynomial_ref p(m_pm); polynomial_ref p(m_pm);
unsigned sz = ps.size(); unsigned sz = ps.size();
for (unsigned k = 0; k < sz; k++) { for (unsigned k = 0; k < sz; k++) {

1
src/nlsat/nlsat_interval_set.cpp
View file

@ -78,6 +78,7 @@ namespace nlsat {
auto s = am.compare(i.m_lower, i.m_upper); auto s = am.compare(i.m_lower, i.m_upper);
TRACE("nlsat_interval", tout << "lower: "; am.display_decimal(tout, i.m_lower); tout << ", upper: "; am.display_decimal(tout, i.m_upper); TRACE("nlsat_interval", tout << "lower: "; am.display_decimal(tout, i.m_lower); tout << ", upper: "; am.display_decimal(tout, i.m_upper);
tout << "\ns: " << s << "\n";); tout << "\ns: " << s << "\n";);
(void)s;
SASSERT(s <= 0); SASSERT(s <= 0);
SASSERT(!is_zero(s) || !i.m_lower_open && !i.m_upper_open); SASSERT(!is_zero(s) || !i.m_lower_open && !i.m_upper_open);
} }

2
src/nlsat/nlsat_solver.cpp
View file

@ -1795,7 +1795,7 @@ namespace nlsat {
} }
void resolve_clause(bool_var b, clause const & c) { void resolve_clause(bool_var b, clause const & c) {
TRACE("nlsat_resolve", tout << "resolving clause for b: " << b << "\n";); TRACE("nlsat_resolve", tout << "resolving clause for b: " << b << "\n"; display(tout, c) << "\n";);
resolve_clause(b, c.size(), c.c_ptr()); resolve_clause(b, c.size(), c.c_ptr());
m_lemma_assumptions = m_asm.mk_join(static_cast<_assumption_set>(c.assumptions()), m_lemma_assumptions); m_lemma_assumptions = m_asm.mk_join(static_cast<_assumption_set>(c.assumptions()), m_lemma_assumptions);
} }