From fb824bee540b6ac52706aac5d8a2a0f34d00fc8e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 16 Mar 2024 13:02:26 -0700 Subject: [PATCH] inline unfolding if it is linear or constant. --- src/sat/smt/polysat/ule_constraint.cpp | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/sat/smt/polysat/ule_constraint.cpp b/src/sat/smt/polysat/ule_constraint.cpp index e8029d417..410a37dea 100644 --- a/src/sat/smt/polysat/ule_constraint.cpp +++ b/src/sat/smt/polysat/ule_constraint.cpp @@ -264,6 +264,11 @@ namespace polysat { 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()); for (auto v : m_rhs.free_vars()) if (!vars().contains(v))