mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-15 08:44:10 +00:00
Code Activity

Disable operator== for lar_term

Browse source 
The operator== for lar_term was never intended to be used.
This changes physically disables it to identify what happens to depend
on the operator.
This commit is contained in:
Arie Gurfinkel 2026-04-12 09:38:16 -04:00
parent fe100e7865
commit 81f242e45f
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/math/lp/lar_term.h
View file

@ -129,8 +129,8 @@ public:
add_monomial(a, v1);
add_monomial(b, v2);
}
bool operator==(const lar_term & a) const { return false; } // take care not to create identical terms
bool operator!=(const lar_term & a) const { return ! (*this == a);}
bool operator==(const lar_term & a) const = delete; // take care not to create identical terms
bool operator!=(const lar_term & a) const = delete;
// some terms get used in add constraint
// it is the same as the offset in the m_constraints