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

Work around missing lar_term==

Browse source 
Previous commit disabled lar_term==. This is the only use of the
operator that seems meaningful. Changed it to compare by references
instead.

Compiles, but not sure this is the best solution.
This commit is contained in:
Arie Gurfinkel 2026-04-12 09:39:20 -04:00
parent 81f242e45f
commit 276b00db5b
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -42,7 +42,7 @@ namespace nla {
ineq(lpvar v, lp::lconstraint_kind cmp, int i): m_cmp(cmp), m_term(v), m_rs(rational(i)) {}
ineq(lpvar v, lp::lconstraint_kind cmp, rational const& r): m_cmp(cmp), m_term(v), m_rs(r) {}
bool operator==(const ineq& a) const {
return m_cmp == a.m_cmp && m_term == a.m_term && m_rs == a.m_rs;
return m_cmp == a.m_cmp && &m_term == &a.m_term && m_rs == a.m_rs;
}
const lp::lar_term& term() const { return m_term; };
lp::lconstraint_kind cmp() const { return m_cmp; };