mirror of
https://github.com/Z3Prover/z3
synced 2025-04-12 12:08:18 +00:00
add this qualifier for build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
29a49f4427
commit
2ab0f281f3
|
@ -89,7 +89,7 @@ public:
|
||||||
// if (choices.size() == 1)
|
// if (choices.size() == 1)
|
||||||
// return choices[0];
|
// return choices[0];
|
||||||
|
|
||||||
// unsigned k = m_settings.random_next() % choices.size();
|
// unsigned k = this->m_settings.random_next() % choices.size();
|
||||||
// return choices[k];
|
// return choices[k];
|
||||||
// #endif
|
// #endif
|
||||||
// }
|
// }
|
||||||
|
@ -287,7 +287,7 @@ public:
|
||||||
choices.clear();
|
choices.clear();
|
||||||
choices.push_back(&rc);
|
choices.push_back(&rc);
|
||||||
} else if (damage == num_of_non_free_basics &&
|
} else if (damage == num_of_non_free_basics &&
|
||||||
this->m_A.m_columns[j].size() <= len && (m_settings.random_next() % 2)) {
|
this->m_A.m_columns[j].size() <= len && (this->m_settings.random_next() % 2)) {
|
||||||
choices.push_back(&rc);
|
choices.push_back(&rc);
|
||||||
len = this->m_A.m_columns[j].size();
|
len = this->m_A.m_columns[j].size();
|
||||||
}
|
}
|
||||||
|
@ -299,7 +299,7 @@ public:
|
||||||
return -1;
|
return -1;
|
||||||
}
|
}
|
||||||
const row_cell<T>* rc = choices.size() == 1? choices[0] :
|
const row_cell<T>* rc = choices.size() == 1? choices[0] :
|
||||||
choices[m_settings.random_next() % choices.size()];
|
choices[this->m_settings.random_next() % choices.size()];
|
||||||
|
|
||||||
a_ent = rc->m_value;
|
a_ent = rc->m_value;
|
||||||
return rc->m_j;
|
return rc->m_j;
|
||||||
|
|
Loading…
Reference in a new issue