From b264e6c2904456beae27ce19ec4997251034e42c Mon Sep 17 00:00:00 2001
From: Clemens Eisenhofer <56730610+CEisenhofer@users.noreply.github.com>
Date: Tue, 12 Apr 2022 12:29:53 +0200
Subject: [PATCH] Reverted reusing can_propagate (#5966)

* Fixed registering expressions in push/pop

* Reused existing function

* Reverted reusing can_propagate
---
 src/smt/theory_user_propagator.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/smt/theory_user_propagator.cpp b/src/smt/theory_user_propagator.cpp
index daded32c7..f783f22fb 100644
--- a/src/smt/theory_user_propagator.cpp
+++ b/src/smt/theory_user_propagator.cpp
@@ -133,7 +133,7 @@ final_check_status theory_user_propagator::final_check_eh() {
     }
     propagate();
     // check if it became inconsistent or something new was propagated/registered
-    bool done = !can_propagate() && !ctx.inconsistent();
+    bool done = (sz1 == m_prop.size()) && (sz2 == m_expr2var.size()) && !ctx.inconsistent();
     return done ? FC_DONE : FC_CONTINUE;
 }