From 65b678dd425ffebd8be8e232b8799ae3a4c387db Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 22 Dec 2024 06:14:38 +0100
Subject: [PATCH] use bail_out instead of early return to ensure marks are
 cleared

---
 src/sat/smt/pb_solver.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/sat/smt/pb_solver.cpp b/src/sat/smt/pb_solver.cpp
index b81c9d059..6dbc5a99d 100644
--- a/src/sat/smt/pb_solver.cpp
+++ b/src/sat/smt/pb_solver.cpp
@@ -712,7 +712,7 @@ namespace pb {
                 auto cindex = js.get_ext_justification_idx();
                 auto* ext = sat::constraint_base::to_extension(cindex);
                 if (ext != this) 
-                    return l_undef;
+                    goto bail_out;
                 
                 constraint& cnstr = index2constraint(cindex);
                 ++m_stats.m_num_resolves;