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

merge

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-05-15 12:00:25 -07:00
parent 1028c80851
commit 186a3c58e5
1 changed files with 5 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/math/simplex/sparse_matrix_def.h
View file

@ -299,7 +299,8 @@ namespace simplex {
template<typename Ext> template<typename Ext>
void sparse_matrix<Ext>::add_var(row dst, numeral const& n, var_t v) { void sparse_matrix<Ext>::add_var(row dst, numeral const& n, var_t v) {
if (m.is_zero(n)) return; if (m.is_zero(n))
return;
_row& r = m_rows[dst.id()]; _row& r = m_rows[dst.id()];
column& c = m_columns[v]; column& c = m_columns[v];
unsigned r_idx; unsigned r_idx;
@ -318,7 +319,9 @@ namespace simplex {
*/ */
template<typename Ext> template<typename Ext>
void sparse_matrix<Ext>::add(row row1, numeral const& n, row row2) { void sparse_matrix<Ext>::add(row row1, numeral const& n, row row2) {
if (m.is_zero(n)) return;
if (m.is_zero(n))
return;
m_stats.m_add_rows++; m_stats.m_add_rows++;
_row & r1 = m_rows[row1.id()]; _row & r1 = m_rows[row1.id()];