Lev (Z3Prover#26)

* local changes Signed-off-by: Nikolaj Bjorner <[email protected]> * fix warnings and returning index to add_var_bound Signed-off-by: Nikolaj Bjorner <[email protected]>
NikolajBjorner · Aug 13, 2016 · d604308 · d604308
1 parent 48d660a
commit d604308
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 4 deletions.
diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp
@@ -518,7 +518,7 @@ void lar_solver::map_var_indices_to_columns_of_A() {
 // }
 template <typename U, typename V>
 void lar_solver::prepare_core_solver_fields_with_signature(static_matrix<U, V> & A, std::vector<V> & x,
-    std::vector<V> & low_bound,
+                                                           std::vector<V> & low_bound,
                                                            std::vector<V> & upper_bound, const lar_solution_signature & signature) {
     create_matrix_A(A);
     fill_bounds_for_core_solver(low_bound, upper_bound);

diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h
@@ -211,9 +211,8 @@ class lar_solver : public column_namer {
         }
         std::cout << "adding bound for a term" << std::endl;
         m_mpq_lar_core_solver.print_linear_combination_of_column_indices(m_terms()[adjust_term_index(j)].m_coeffs, std::cout);
-        std::cout << "\n";
         // it is a term!
-        add_constraint(m_terms()[adjust_term_index(j)].m_coeffs, kind, right_side);
+        return add_constraint(m_terms()[adjust_term_index(j)].m_coeffs, kind, right_side);
     }
 
     constraint_index add_constraint(const std::vector<std::pair<mpq, var_index>>& left_side, lconstraint_kind kind_par, mpq right_side_par);

diff --git a/src/util/lp/stacked_vector.h b/src/util/lp/stacked_vector.h
@@ -93,7 +93,7 @@ template < typename B> class stacked_vector {
                 m_vector[t.first] = t.second;
             }
             lean_assert(d.m_deb_copy.size() == m_vector.size());
-            for (int i = 0; i < m_vector.size();i++){
+            for (unsigned i = 0; i < m_vector.size();i++){
                 std::cout << "i = " << i << std::endl;
                 lean_assert(d.m_deb_copy[i] == m_vector[i]);
             }