mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-23 06:13:40 +00:00
Code Activity

add missing initialization

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-05-24 14:47:09 -07:00
parent d45c56da3f
commit 80bb084611
2 changed files with 3 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/util/lp/lar_solver.cpp
View file

@ -31,7 +31,9 @@ lar_solver::lar_solver() : m_status(OPTIMAL),
m_infeasible_column_index(-1), m_infeasible_column_index(-1),
m_terms_start_index(1000000), m_terms_start_index(1000000),
m_mpq_lar_core_solver(m_settings, *this) m_mpq_lar_core_solver(m_settings, *this)
{} {
m_nra = alloc(nra::solver, *this);
}
void lar_solver::set_propagate_bounds_on_pivoted_rows_mode(bool v) { void lar_solver::set_propagate_bounds_on_pivoted_rows_mode(bool v) {
m_mpq_lar_core_solver.m_r_solver.m_pivoted_rows = v? (& m_rows_with_changed_bounds) : nullptr; m_mpq_lar_core_solver.m_r_solver.m_pivoted_rows = v? (& m_rows_with_changed_bounds) : nullptr;

1
src/util/lp/nra_solver.cpp
View file

@ -30,7 +30,6 @@ namespace nra {
vector<mon_eq> m_monomials; vector<mon_eq> m_monomials;
unsigned_vector m_lim; unsigned_vector m_lim;
mutable std::unordered_map<lean::var_index, rational> m_variable_values; // current model mutable std::unordered_map<lean::var_index, rational> m_variable_values; // current model
vector<std::pair<rational, unsigned>> m_core;
imp(lean::lar_solver& s): imp(lean::lar_solver& s):
s(s) { s(s) {