diff --git a/src/sat/smt/pb_internalize.cpp b/src/sat/smt/pb_internalize.cpp
index f30d25b31..eae1bbe5a 100644
--- a/src/sat/smt/pb_internalize.cpp
+++ b/src/sat/smt/pb_internalize.cpp
@@ -18,6 +18,7 @@ Author:
 
 #include "sat/smt/pb_solver.h"
 #include "ast/pb_decl_plugin.h"
+#include "sat/smt/euf_solver.h"
 
 namespace pb {
 
@@ -27,8 +28,12 @@ namespace pb {
 
     literal solver::internalize(expr* e, bool sign, bool root, bool redundant) {
         flet<bool> _redundant(m_is_redundant, redundant);
-        if (m_pb.is_pb(e)) 
-            return internalize_pb(e, sign, root);
+        if (m_pb.is_pb(e)) {
+            sat::literal lit = internalize_pb(e, sign, root);
+            if (m_ctx && !root && lit != sat::null_literal)
+                m_ctx->attach_lit(lit, e);            
+            return lit;
+        }
         UNREACHABLE();
         return sat::null_literal;
     }
diff --git a/src/sat/smt/pb_solver.cpp b/src/sat/smt/pb_solver.cpp
index ff4d9fd36..69920342d 100644
--- a/src/sat/smt/pb_solver.cpp
+++ b/src/sat/smt/pb_solver.cpp
@@ -1338,7 +1338,9 @@ namespace pb {
     }
 
     solver::solver(euf::solver& ctx, euf::theory_id id) :
-        solver(ctx.get_manager(), ctx.get_si(), id) {}
+        solver(ctx.get_manager(), ctx.get_si(), id) {
+        m_ctx = &ctx;
+    }
 
     solver::solver(ast_manager& m, sat::sat_internalizer& si, euf::theory_id id)
         : euf::th_solver(m, symbol("ba"), id),
diff --git a/src/sat/smt/pb_solver.h b/src/sat/smt/pb_solver.h
index c19facf34..09c0e47e0 100644
--- a/src/sat/smt/pb_solver.h
+++ b/src/sat/smt/pb_solver.h
@@ -80,7 +80,8 @@ namespace pb {
         sat::sat_internalizer&      si;
         pb_util                m_pb;
 
-        sat::lookahead*        m_lookahead{ nullptr };
+        sat::lookahead*        m_lookahead = nullptr;
+        euf::solver*           m_ctx = nullptr;
         stats                  m_stats; 
         small_object_allocator m_allocator;