mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-09-03 08:38:06 +00:00
Code Activity

work on seed_properties

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-08-28 16:53:57 -10:00
parent 345091d97e
commit 70aafea26c
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/nlsat/levelwise.cpp
View file

@ -186,8 +186,8 @@ namespace nlsat {
poly* p2 = root_vals[j+1].second; poly* p2 = root_vals[j+1].second;
if (p1 == p2) continue; // the delineability of p1 will be handled by an_del property above if (p1 == p2) continue; // the delineability of p1 will be handled by an_del property above
unsigned id1 = m_pm.id(p1);// polynomial::manager::id(polynomial_ref(p1, m_pm)); unsigned id1 = m_pm.id(p1);
unsigned id2 = polynomial::manager::id(polynomial_ref(p2, m_pm)); unsigned id2 = m_pm.id(p2);
std::pair<unsigned,unsigned> key = id1 < id2 ? std::make_pair(id1, id2) : std::make_pair(id2, id1); std::pair<unsigned,unsigned> key = id1 < id2 ? std::make_pair(id1, id2) : std::make_pair(id2, id1);
if (added_pairs.find(key) != added_pairs.end()) if (added_pairs.find(key) != added_pairs.end())
continue; continue;