mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

address clang warnings

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-11-11 07:16:46 -08:00
parent 0c1b68b598
commit 20598e3bd2
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/tactic/fd_solver/smtfd_solver.cpp
View file

@ -1531,7 +1531,6 @@ namespace smtfd {
unsigned_vector m_toggles_lim; unsigned_vector m_toggles_lim;
model_ref m_model; model_ref m_model;
std::string m_reason_unknown; std::string m_reason_unknown;
unsigned m_max_lemmas;
stats m_stats; stats m_stats;
unsigned m_max_conflicts; unsigned m_max_conflicts;
obj_hashtable<quantifier> m_enforced_quantifier; obj_hashtable<quantifier> m_enforced_quantifier;
@ -1644,7 +1643,7 @@ namespace smtfd {
expr_ref_vector terms(core); expr_ref_vector terms(core);
terms.append(m_axioms); terms.append(m_axioms);
for (unsigned round = 0; !m_context.at_max() && m_context.add_theory_axioms(terms, round); ++round); for (unsigned round = 0; !m_context.at_max() && m_context.add_theory_axioms(terms, round); ++round) {}
TRACE("smtfd", m_context.display(tout);); TRACE("smtfd", m_context.display(tout););
for (expr* f : m_context) { for (expr* f : m_context) {

1
src/test/lp/lp.cpp
View file

@ -1776,6 +1776,7 @@ void solve_rational() {
solver.find_maximal_solution(); solver.find_maximal_solution();
lp_assert(solver.get_status() == lp_status::OPTIMAL); lp_assert(solver.get_status() == lp_status::OPTIMAL);
for (const auto & it : expected_sol) { for (const auto & it : expected_sol) {
(void)it;
lp_assert(it.second == solver.get_column_value_by_name(it.first)); lp_assert(it.second == solver.get_column_value_by_name(it.first));
} }
} }