diff --git a/src/muz/spacer/spacer_antiunify.cpp b/src/muz/spacer/spacer_antiunify.cpp
index 6c382a723..7dae59b6a 100644
--- a/src/muz/spacer/spacer_antiunify.cpp
+++ b/src/muz/spacer/spacer_antiunify.cpp
@@ -335,8 +335,8 @@ bool naive_convex_closure::compute_closure(anti_unifier& au, ast_manager& m,
// for each substitution entry
bool is_first_key = true;
- unsigned lower_bound;
- unsigned upper_bound;
+ unsigned lower_bound = 0;
+ unsigned upper_bound = 0;
for (const auto& pair : au.get_substitution(0)) {
// construct vector
expr* key = &pair.get_key();
@@ -355,8 +355,8 @@ bool naive_convex_closure::compute_closure(anti_unifier& au, ast_manager& m,
}
// check whether vector represents interval
- unsigned current_lower_bound;
- unsigned current_upper_bound;
+ unsigned current_lower_bound = 0;
+ unsigned current_upper_bound = 0;
// if vector represents interval
if (get_range(entries, current_lower_bound, current_upper_bound)) {
diff --git a/src/muz/spacer/spacer_farkas_learner.cpp b/src/muz/spacer/spacer_farkas_learner.cpp
index 29d238cc9..47bc474ef 100644
--- a/src/muz/spacer/spacer_farkas_learner.cpp
+++ b/src/muz/spacer/spacer_farkas_learner.cpp
@@ -389,11 +389,11 @@ void farkas_learner::get_lemmas(proof* root, expr_set const& bs, expr_ref_vector
simplify_bounds(lemmas);
}
-void farkas_learner::get_asserted(proof* p, expr_set const& bs, ast_mark& b_closed, obj_hashtable<expr>& lemma_set, expr_ref_vector& lemmas)
+void farkas_learner::get_asserted(proof* p0, expr_set const& bs, ast_mark& b_closed, obj_hashtable<expr>& lemma_set, expr_ref_vector& lemmas)
{
ast_manager& m = lemmas.get_manager();
ast_mark visited;
- proof* p0 = p;
+ proof* p = p0;
ptr_vector<proof> todo;
todo.push_back(p);
diff --git a/src/muz/spacer/spacer_generalizers.cpp b/src/muz/spacer/spacer_generalizers.cpp
index 9f8757024..40e5c2c4d 100644
--- a/src/muz/spacer/spacer_generalizers.cpp
+++ b/src/muz/spacer/spacer_generalizers.cpp
@@ -133,9 +133,7 @@ void unsat_core_generalizer::operator()(lemma_ref &lemma)
unsigned uses_level;
expr_ref_vector core(m);
- bool r;
- r = pt.is_invariant(lemma->level(), lemma->get_expr(), uses_level, &core);
- SASSERT(r);
+ VERIFY(pt.is_invariant(lemma->level(), lemma->get_expr(), uses_level, &core));
CTRACE("spacer", old_sz > core.size(),
tout << "unsat core reduced lemma from: "
@@ -185,6 +183,7 @@ void lemma_array_eq_generalizer::operator() (lemma_ref &lemma)
// -- find array constants
ast_manager &m = lemma->get_ast_manager();
manager &pm = m_ctx.get_manager();
+ (void)pm;
expr_ref_vector core(m);
expr_ref v(m);
diff --git a/src/muz/spacer/spacer_legacy_frames.cpp b/src/muz/spacer/spacer_legacy_frames.cpp
index 77e6f5650..6c732ecc0 100644
--- a/src/muz/spacer/spacer_legacy_frames.cpp
+++ b/src/muz/spacer/spacer_legacy_frames.cpp
@@ -79,6 +79,7 @@ bool pred_transformer::legacy_frames::propagate_to_next_level(unsigned src_level
{
ast_manager &m = m_pt.get_ast_manager();
+ (void) m;
if (m_levels.size() <= src_level) { return true; }
if (m_levels [src_level].empty()) { return true; }
diff --git a/src/muz/spacer/spacer_prop_solver.cpp b/src/muz/spacer/spacer_prop_solver.cpp
index 27225315c..719443457 100644
--- a/src/muz/spacer/spacer_prop_solver.cpp
+++ b/src/muz/spacer/spacer_prop_solver.cpp
@@ -264,6 +264,7 @@ lbool prop_solver::check_assumptions(const expr_ref_vector & _hard,
else { m_ctx->assert_expr(bg[i]); }
unsigned soft_sz = soft.size();
+ (void) soft_sz;
lbool res = internal_check_assumptions(hard, soft);
if (!m_use_push_bg) { m_ctx->pop(1); }
diff --git a/src/muz/spacer/spacer_qe_project.cpp b/src/muz/spacer/spacer_qe_project.cpp
index 62c9c2643..c06854cb0 100644
--- a/src/muz/spacer/spacer_qe_project.cpp
+++ b/src/muz/spacer/spacer_qe_project.cpp
@@ -788,7 +788,7 @@ namespace qe {
}
unsigned find_max(model& mdl, bool do_pos) {
- unsigned result;
+ unsigned result = UINT_MAX;
bool found = false;
bool found_strict = false;
rational found_val (0), r, r_plus_x, found_c;
@@ -2078,6 +2078,7 @@ namespace qe {
sort* v_sort = m.get_sort (v);
sort* val_sort = get_array_range (v_sort);
sort* idx_sort = get_array_domain (v_sort, 0);
+ (void) idx_sort;
unsigned start = m_idx_reprs.size (); // append at the end
diff --git a/src/muz/spacer/spacer_unsat_core_plugin.cpp b/src/muz/spacer/spacer_unsat_core_plugin.cpp
index a352a2460..66abb32c6 100644
--- a/src/muz/spacer/spacer_unsat_core_plugin.cpp
+++ b/src/muz/spacer/spacer_unsat_core_plugin.cpp
@@ -444,10 +444,10 @@ void unsat_core_plugin_farkas_lemma::compute_linear_combination(const vector<rat
}
- void unsat_core_plugin_farkas_lemma_bounded::finalize()
- {
- if(m_linear_combinations.empty())
- {return;}
+ void unsat_core_plugin_farkas_lemma_bounded::finalize() {
+ if (m_linear_combinations.empty()) {
+ return;
+ }
DEBUG_CODE(
for (auto& linear_combination : m_linear_combinations) {
SASSERT(linear_combination.size() > 0);
@@ -457,12 +457,9 @@ void unsat_core_plugin_farkas_lemma::compute_linear_combination(const vector<rat
ptr_vector<app> ordered_basis;
obj_map<app, unsigned> map;
unsigned counter = 0;
- for (const auto& linear_combination : m_linear_combinations)
- {
- for (const auto& pair : linear_combination)
- {
- if (!map.contains(pair.first))
- {
+ for (const auto& linear_combination : m_linear_combinations) {
+ for (const auto& pair : linear_combination) {
+ if (!map.contains(pair.first)) {
ordered_basis.push_back(pair.first);
map.insert(pair.first, counter++);
}
@@ -472,14 +469,12 @@ void unsat_core_plugin_farkas_lemma::compute_linear_combination(const vector<rat
// 2. populate matrix
spacer_matrix matrix(m_linear_combinations.size(), ordered_basis.size());
- for (unsigned i=0; i < m_linear_combinations.size(); ++i)
- {
+ for (unsigned i=0; i < m_linear_combinations.size(); ++i) {
auto linear_combination = m_linear_combinations[i];
- for (const auto& pair : linear_combination)
- {
+ for (const auto& pair : linear_combination) {
matrix.set(i, map[pair.first], pair.second);
}
- }
+ }
matrix.print_matrix();
// 3. normalize matrix to integer values
@@ -489,8 +484,7 @@ void unsat_core_plugin_farkas_lemma::compute_linear_combination(const vector<rat
arith_util util(m);
vector<expr_ref_vector> coeffs;
- for (unsigned i=0; i < matrix.num_rows(); ++i)
- {
+ for (unsigned i=0; i < matrix.num_rows(); ++i) {
coeffs.push_back(expr_ref_vector(m));
}
@@ -532,19 +526,17 @@ void unsat_core_plugin_farkas_lemma::compute_linear_combination(const vector<rat
}
// assert bounds for all s_jn
- for (unsigned l=0; l < n; ++l)
- {
- for (unsigned j=0; j < matrix.num_cols(); ++j)
- {
+ for (unsigned l=0; l < n; ++l) {
+ for (unsigned j=0; j < matrix.num_cols(); ++j) {
expr* s_jn = bounded_vectors[j][l].get();
-
+
expr_ref lb(util.mk_le(util.mk_int(0), s_jn), m);
expr_ref ub(util.mk_le(s_jn, util.mk_int(1)), m);
s->assert_expr(lb);
s->assert_expr(ub);
- }
}
-
+ }
+
// assert: forall i,j: a_ij = sum_k w_ik * s_jk
for (unsigned i=0; i < matrix.num_rows(); ++i)
{
@@ -568,34 +560,30 @@ void unsat_core_plugin_farkas_lemma::compute_linear_combination(const vector<rat
lbool res = s->check_sat(0,0);
// if sat extract model and add corresponding linear combinations to core
- if (res == lbool::l_true)
- {
+ if (res == lbool::l_true) {
model_ref model;
s->get_model(model);
-
- for (int k=0; k < n; ++k)
- {
- ptr_vector<app> literals;
- vector<rational> coefficients;
- for (unsigned j=0; j < matrix.num_cols(); ++j)
- {
+
+ for (unsigned k=0; k < n; ++k) {
+ ptr_vector<app> literals;
+ vector<rational> coefficients;
+ for (unsigned j=0; j < matrix.num_cols(); ++j) {
expr_ref evaluation(m);
-
+
model.get()->eval(bounded_vectors[j][k].get(), evaluation, false);
- if (!util.is_zero(evaluation))
- {
+ if (!util.is_zero(evaluation)) {
literals.push_back(ordered_basis[j]);
coefficients.push_back(rational(1));
- }
- }
+ }
+ }
SASSERT(!literals.empty()); // since then previous outer loop would have found solution already
- expr_ref linear_combination(m);
- compute_linear_combination(coefficients, literals, linear_combination);
-
- m_learner.add_lemma_to_core(linear_combination);
- }
+ expr_ref linear_combination(m);
+ compute_linear_combination(coefficients, literals, linear_combination);
+
+ m_learner.add_lemma_to_core(linear_combination);
+ }
return;
- }
+ }
}
}