diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp
index e2b116ea2..9f747090a 100644
--- a/src/sat/smt/euf_internalize.cpp
+++ b/src/sat/smt/euf_internalize.cpp
@@ -224,6 +224,14 @@ namespace euf {
             return;
         }
 
+        // check if it is trivial
+        expr_mark visited;
+        for (expr* arg : *e) {
+            if (visited.is_marked(arg))
+                return;
+            visited.mark(arg);
+        }
+
         static const unsigned distinct_max_args = 32;
         if (sz <= distinct_max_args) {
             sat::literal_vector lits;
@@ -248,7 +256,8 @@ namespace euf {
             func_decl_ref g(m.mk_fresh_func_decl("dist-g", "", 1, &u_ptr, srt), m);
             expr_ref a(m.mk_fresh_const("a", u), m);
             expr_ref_vector eqs(m);
-            for (expr* arg : *e) {
+
+            for (expr* arg : *e) {                
                 expr_ref fapp(m.mk_app(f, arg), m);
                 expr_ref gapp(m.mk_app(g, fapp.get()), m);
                 expr_ref eq = mk_eq(gapp, arg);
diff --git a/src/sat/smt/pb_pb.cpp b/src/sat/smt/pb_pb.cpp
index 1c016311e..6665e19f0 100644
--- a/src/sat/smt/pb_pb.cpp
+++ b/src/sat/smt/pb_pb.cpp
@@ -39,6 +39,8 @@ namespace pb {
         m_max_sum(0) {
         for (unsigned i = 0; i < size(); ++i) {
             m_wlits[i] = wlits[i];
+            if (wlits[i].first > k)
+                m_wlits[i].first = k;
         }
         update_max_sum();
     }
@@ -47,9 +49,8 @@ namespace pb {
         m_max_sum = 0;
         for (unsigned i = 0; i < size(); ++i) {
             m_wlits[i].first = std::min(k(), m_wlits[i].first);
-            if (m_max_sum + m_wlits[i].first < m_max_sum) {
+            if (m_max_sum + m_wlits[i].first < m_max_sum) 
                 throw default_exception("addition of pb coefficients overflows");
-            }
             m_max_sum += m_wlits[i].first;
         }
     }
diff --git a/src/sat/smt/pb_solver.cpp b/src/sat/smt/pb_solver.cpp
index d1f101582..c3e43bfbe 100644
--- a/src/sat/smt/pb_solver.cpp
+++ b/src/sat/smt/pb_solver.cpp
@@ -1354,7 +1354,6 @@ namespace pb {
           si(si), m_pb(m),
           m_lookahead(nullptr), 
           m_constraint_id(0), m_ba(*this), m_sort(m_ba) {
-        TRACE("pb", tout << this << "\n";);
         m_num_propagations_since_pop = 0;
     }
 
@@ -1432,6 +1431,7 @@ namespace pb {
         }     
         if (!c->well_formed()) 
             IF_VERBOSE(0, verbose_stream() << *c << "\n");
+        SASSERT(c->well_formed());
         VERIFY(c->well_formed());
         if (m_solver && m_solver->get_config().m_drat) {
             auto * out = s().get_drat().out();