From aafd9039db24eb90bc911bc22be29e353881fb33 Mon Sep 17 00:00:00 2001
From: Clemens Eisenhofer <Clemens.Eisenhofer@tuwien.ac.at>
Date: Mon, 9 Jan 2023 14:14:19 +0100
Subject: [PATCH] Bugfix

---
 src/math/polysat/saturation.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/math/polysat/saturation.cpp b/src/math/polysat/saturation.cpp
index 192274efa..fd70cda3d 100644
--- a/src/math/polysat/saturation.cpp
+++ b/src/math/polysat/saturation.cpp
@@ -1258,11 +1258,11 @@ namespace polysat {
             }
             else if (c->is_umul_ovfl()) {
                 auto const& ovf = c->to_umul_ovfl();
+                m_lemma.reset();
                 auto [lhs_new, changed_lhs] = m_parity_tracker.eliminate_variable(*this, x, a, b, ovf.p(), m_lemma);
                 auto [rhs_new, changed_rhs] = m_parity_tracker.eliminate_variable(*this, x, a, b, ovf.q(), m_lemma);
                 if (!changed_lhs && !changed_rhs)
                     continue;
-                m_lemma.reset();
                 m_lemma.insert(~c);
                 m_lemma.insert_eval(~s.eq(y));