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

inline unfolding if it is linear or constant.

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-03-16 13:02:26 -07:00
parent 3555b25317
commit fb824bee54
1 changed files with 5 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/sat/smt/polysat/ule_constraint.cpp
View file

@ -264,6 +264,11 @@ namespace polysat {
SASSERT_EQ(m_lhs.power_of_2(), m_rhs.power_of_2()); SASSERT_EQ(m_lhs.power_of_2(), m_rhs.power_of_2());
if (ul.is_linear_or_value())
m_lhs = ul;
if (ur.is_linear_or_value())
m_rhs = ur;
vars().append(m_lhs.free_vars()); vars().append(m_lhs.free_vars());
for (auto v : m_rhs.free_vars()) for (auto v : m_rhs.free_vars())
if (!vars().contains(v)) if (!vars().contains(v))