mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 03:45:51 +00:00
Code Activity

add a unit test for monics, plus some cosmetic changes

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-03-12 18:22:53 -07:00
parent 0207878f5f
commit 26631ce38d
5 changed files with 103 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/lp/var_eqs.h
View file

@ -108,6 +108,8 @@ public:
\brief merge equivalence classes for v1, v2 with justification j
*/
void merge(signed_var v1, signed_var v2, eq_justification const& j) {
if (v1 == v2)
return;
unsigned max_i = std::max(v1.index(), v2.index()) + 2;
m_eqs.reserve(max_i);
while (m_uf.get_num_vars() <= max_i) m_uf.mk_var();