diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 217fdaa26..6c6145ed4 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -345,6 +345,21 @@ namespace opt {
         m_optsmt.setup(*m_opt_solver.get());
         update_lower();
         
+        // Try to detect and optimize max PB constraints pattern before deciding optimization strategy
+        if (m_objectives.size() > 1) {
+            expr_ref_vector maxsat_terms(m);
+            vector<rational> maxsat_weights;
+            rational maxsat_offset;
+            bool maxsat_neg;
+            symbol maxsat_id;
+            
+            if (detect_max_pb_constraints(maxsat_terms, maxsat_weights, maxsat_offset, maxsat_neg, maxsat_id)) {
+                TRACE(opt, tout << "Max PB pattern detected, switching to single maxsat objective\n";);
+                // The pattern was detected and objectives were modified by detect_max_pb_constraints
+                // Now we have a single objective, so we can process it as such
+            }
+        }
+        
         switch (m_objectives.size()) {
         case 0:
             break;
@@ -1077,12 +1092,135 @@ namespace opt {
             neg = is_max;
             std::ostringstream out;
             out << mk_bounded_pp(orig_term, m, 2) << ':' << index;
-            id = symbol(out.str());
             return true;
         }
         return false;
     }
 
+    bool context::detect_max_pb_constraints(expr_ref_vector& terms, 
+                                           vector<rational>& weights, rational& offset, 
+                                           bool& neg, symbol& id) {
+        // This function detects when we have multiple maximize objectives that are PB constraints
+        // and transforms them to use auxiliary variables.
+        // 
+        // Pattern: maximize { PB1, ..., PBn } where each PB_i is a weighted sum of Boolean variables
+        // Transform to: PB_i >= k => p_i_k for k = 1, ..., max_potential_sum(PB_i)
+        //               maximize sum(p_i_k for all i,k)
+        
+        TRACE(opt, tout << "detect_max_pb_constraints called with " << m_objectives.size() << " objectives\n";);
+        
+        unsigned num_maximize_objs = 0;
+        vector<unsigned> max_indices;
+        vector<expr_ref_vector> pb_terms;
+        vector<vector<rational>> pb_weights;
+        vector<rational> pb_offsets;
+        
+        // First pass: collect all maximize objectives that are PB constraints
+        for (unsigned idx = 0; idx < m_objectives.size(); ++idx) {
+            objective const& obj = m_objectives[idx];
+            TRACE(opt, tout << "Objective " << idx << " type: " << obj.m_type << "\n";);
+            if (obj.m_type == O_MAXIMIZE && obj.m_term) {
+                expr_ref_vector pb_terms_i(m);
+                vector<rational> pb_weights_i;
+                rational pb_offset_i;
+                
+                if (get_pb_sum(obj.m_term, pb_terms_i, pb_weights_i, pb_offset_i)) {
+                    max_indices.push_back(idx);
+                    pb_terms.push_back(pb_terms_i);
+                    pb_weights.push_back(pb_weights_i);
+                    pb_offsets.push_back(pb_offset_i);
+                    num_maximize_objs++;
+                    TRACE(opt, tout << "Objective " << idx << " is a PB constraint with " << pb_terms_i.size() << " terms\n";);
+                }
+            }
+        }
+        
+        TRACE(opt, tout << "Found " << num_maximize_objs << " PB maximize objectives\n";);
+        
+        // Only apply transformation if we have multiple PB maximize objectives
+        if (num_maximize_objs < 2) {
+            return false;
+        }
+        
+        TRACE(opt, tout << "Detected " << num_maximize_objs << " PB maximize objectives, applying transformation\n";);
+        
+        // Clear output vectors
+        terms.reset();
+        weights.reset();
+        offset = rational::zero();
+        neg = true; // We negate because we convert maximize to maxsat (minimizing penalty)
+        
+        arith_util arith(m);
+        
+        // For each PB constraint, create auxiliary variables and constraints
+        for (unsigned i = 0; i < num_maximize_objs; ++i) {
+            expr_ref_vector const& pb_terms_i = pb_terms[i];
+            vector<rational> const& pb_weights_i = pb_weights[i];
+            rational const& pb_offset_i = pb_offsets[i];
+            
+            // Calculate maximum potential sum for this PB constraint
+            rational max_sum = pb_offset_i;
+            for (unsigned j = 0; j < pb_weights_i.size(); ++j) {
+                if (pb_weights_i[j].is_pos()) {
+                    max_sum += pb_weights_i[j];
+                }
+            }
+            
+            TRACE(opt, tout << "PB constraint " << i << " has max sum " << max_sum << "\n";);
+            
+            // Create auxiliary variables p_i_k for k = 1 to max_sum
+            for (rational k = rational::one(); k <= max_sum; k += rational::one()) {
+                std::ostringstream aux_name;
+                aux_name << "pb_aux_" << i << "_" << k.to_string();
+                expr_ref aux_var(m.mk_const(symbol(aux_name.str()), m.mk_bool_sort()), m);
+                
+                // Create PB constraint: sum(pb_weights_i[j] * pb_terms_i[j]) for j
+                expr_ref pb_sum(arith.mk_numeral(pb_offset_i, true), m);
+                for (unsigned j = 0; j < pb_terms_i.size(); ++j) {
+                    expr_ref weighted_term(arith.mk_mul(arith.mk_numeral(pb_weights_i[j], true), 
+                                                      m.mk_ite(pb_terms_i[j], arith.mk_numeral(rational::one(), true), arith.mk_numeral(rational::zero(), true))), m);
+                    pb_sum = arith.mk_add(pb_sum, weighted_term);
+                }
+                
+                // Add constraint: pb_sum >= k => aux_var
+                expr_ref constraint(m.mk_implies(arith.mk_ge(pb_sum, arith.mk_numeral(k, true)), aux_var), m);
+                add_hard_constraint(constraint);
+                
+                // Add auxiliary variable to maximize
+                terms.push_back(aux_var);
+                weights.push_back(rational::one());
+                offset += rational::one();
+            }
+        }
+        
+        // Now modify m_objectives to replace the multiple maximize objectives with a single maxsat objective
+        // Find the first maximize objective to replace
+        unsigned target_index = max_indices[0];
+        objective& obj = m_objectives[target_index];
+        obj.m_id = symbol("max_pb_unified");
+        obj.m_type = O_MAXSMT;
+        obj.m_term = nullptr;
+        obj.m_terms.reset();
+        obj.m_terms.append(terms);
+        obj.m_weights.reset();
+        obj.m_weights.append(weights);
+        obj.m_adjust_value.set_offset(offset);
+        obj.m_adjust_value.set_negate(neg);
+        
+        // Remove other maximize objectives that were converted (in reverse order to maintain indices)
+        for (int i = max_indices.size() - 1; i >= 1; --i) {
+            unsigned idx_to_remove = max_indices[i];
+            m_objectives.erase(m_objectives.begin() + idx_to_remove);
+        }
+        
+        // Create a unique ID for this transformation
+        id = symbol("max_pb_unified");
+        
+        TRACE(opt, tout << "Transformed to " << terms.size() << " auxiliary variables, " << m_objectives.size() << " objectives remaining\n";);
+        
+        return true;
+    }
+
     expr* context::mk_objective_fn(unsigned index, objective_t ty, unsigned sz, expr*const* args) {
         ptr_vector<sort> domain;
         for (unsigned i = 0; i < sz; ++i) {
@@ -1119,6 +1257,7 @@ namespace opt {
     void context::from_fmls(expr_ref_vector const& fmls) {
         TRACE(opt, tout << fmls << "\n";);
         m_hard_constraints.reset();
+        
         for (expr * fml : fmls) {
             app_ref tr(m);
             expr_ref orig_term(m);
diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h
index 991fe16e6..6313aeb00 100644
--- a/src/opt/opt_context.h
+++ b/src/opt/opt_context.h
@@ -313,6 +313,9 @@ namespace opt {
         bool is_maxsat(expr* fml, expr_ref_vector& terms, 
                        vector<rational>& weights, rational& offset, bool& neg, 
                        symbol& id, expr_ref& orig_term, unsigned& index);
+        bool detect_max_pb_constraints(expr_ref_vector& terms, 
+                                     vector<rational>& weights, rational& offset, 
+                                     bool& neg, symbol& id);
         void  purify(app_ref& term);
         app* purify(generic_model_converter_ref& fm, expr* e);
         bool is_mul_const(expr* e);
diff --git a/test_pb_max.smt2 b/test_pb_max.smt2
new file mode 100644
index 000000000..a4eeca282
--- /dev/null
+++ b/test_pb_max.smt2
@@ -0,0 +1,10 @@
+(declare-fun x1 () Bool)
+(declare-fun x2 () Bool)
+(declare-fun y1 () Bool)
+(declare-fun y2 () Bool)
+
+; Create two PB maximize objectives - must be integer expressions
+(maximize (+ (ite x1 2 0) (ite x2 1 0)))  ; PB1: max = 3
+(maximize (+ (ite y1 1 0) (ite y2 2 0)))  ; PB2: max = 3
+
+(check-sat)
\ No newline at end of file
diff --git a/test_pb_optimization b/test_pb_optimization
new file mode 100755
index 000000000..2945f325d
Binary files /dev/null and b/test_pb_optimization differ
diff --git a/test_pb_optimization.cpp b/test_pb_optimization.cpp
new file mode 100644
index 000000000..a62235e65
--- /dev/null
+++ b/test_pb_optimization.cpp
@@ -0,0 +1,104 @@
+#include "z3++.h"
+#include <iostream>
+
+using namespace z3;
+
+void test_pb_max_pattern() {
+    std::cout << "Testing PB max pattern detection\n";
+    
+    context c;
+    
+    // Create boolean variables
+    expr x1 = c.bool_const("x1");
+    expr x2 = c.bool_const("x2");
+    expr x3 = c.bool_const("x3");
+    expr y1 = c.bool_const("y1");
+    expr y2 = c.bool_const("y2");
+    expr z1 = c.bool_const("z1");
+    expr z2 = c.bool_const("z2");
+    expr z3 = c.bool_const("z3");
+    
+    // Create PB constraints like weighted sums
+    expr pb1 = 2*ite(x1, c.int_val(1), c.int_val(0)) + 3*ite(x2, c.int_val(1), c.int_val(0)) + ite(x3, c.int_val(1), c.int_val(0));  // potential max = 6
+    expr pb2 = ite(y1, c.int_val(1), c.int_val(0)) + 2*ite(y2, c.int_val(1), c.int_val(0));                     // potential max = 3  
+    expr pb3 = ite(z1, c.int_val(1), c.int_val(0)) + ite(z2, c.int_val(1), c.int_val(0)) + ite(z3, c.int_val(1), c.int_val(0));       // potential max = 3
+    
+    optimize opt(c);
+    
+    // The pattern the issue might be referring to:
+    // Instead of maximizing pb1 + pb2 + pb3 directly,
+    // we should detect the pattern and introduce auxiliary variables
+    
+    // Current approach: maximize pb1 + pb2 + pb3
+    opt.maximize(pb1 + pb2 + pb3);
+    
+    std::cout << "check: " << opt.check() << std::endl;
+    
+    if (opt.check() == sat) {
+        model m = opt.get_model();
+        std::cout << "Model: " << m << std::endl;
+        
+        // Get objective values
+        std::cout << "Objectives: " << opt.objectives().size() << std::endl;
+    }
+}
+
+void test_pb_max_with_constraints() {
+    std::cout << "\nTesting what the issue might want - auxiliary variables\n";
+    
+    context c;
+    
+    // Create boolean variables
+    expr x1 = c.bool_const("x1");
+    expr x2 = c.bool_const("x2");
+    expr y1 = c.bool_const("y1");
+    expr y2 = c.bool_const("y2");
+    
+    // PB expressions
+    expr pb1 = 2*ite(x1, c.int_val(1), c.int_val(0)) + ite(x2, c.int_val(1), c.int_val(0));  // max = 3
+    expr pb2 = ite(y1, c.int_val(1), c.int_val(0)) + 2*ite(y2, c.int_val(1), c.int_val(0));  // max = 3
+    
+    optimize opt(c);
+    
+    // What the issue might want: auxiliary variables p_k for each threshold k
+    // For pb1: p1_1, p1_2, p1_3 where pb1 >= k => p1_k
+    // For pb2: p2_1, p2_2, p2_3 where pb2 >= k => p2_k
+    // Then maximize: p1_1 + p1_2 + p1_3 + p2_1 + p2_2 + p2_3
+    
+    expr p1_1 = c.bool_const("p1_1");
+    expr p1_2 = c.bool_const("p1_2");
+    expr p1_3 = c.bool_const("p1_3");
+    expr p2_1 = c.bool_const("p2_1");
+    expr p2_2 = c.bool_const("p2_2");
+    expr p2_3 = c.bool_const("p2_3");
+    
+    // Add constraints: pb_i >= k => p_k
+    opt.add(implies(pb1 >= 1, p1_1));
+    opt.add(implies(pb1 >= 2, p1_2));
+    opt.add(implies(pb1 >= 3, p1_3));
+    opt.add(implies(pb2 >= 1, p2_1));
+    opt.add(implies(pb2 >= 2, p2_2));
+    opt.add(implies(pb2 >= 3, p2_3));
+    
+    // Maximize auxiliary variables
+    opt.maximize(ite(p1_1, c.int_val(1), c.int_val(0)) + ite(p1_2, c.int_val(1), c.int_val(0)) + ite(p1_3, c.int_val(1), c.int_val(0)) + ite(p2_1, c.int_val(1), c.int_val(0)) + ite(p2_2, c.int_val(1), c.int_val(0)) + ite(p2_3, c.int_val(1), c.int_val(0)));
+    
+    std::cout << "check: " << opt.check() << std::endl;
+    
+    if (opt.check() == sat) {
+        model m = opt.get_model();
+        std::cout << "Model: " << m << std::endl;
+        
+        // Evaluate original PB expressions
+        std::cout << "pb1 = " << m.eval(pb1) << std::endl;
+        std::cout << "pb2 = " << m.eval(pb2) << std::endl;
+        
+        std::cout << "Objectives: " << opt.objectives().size() << std::endl;
+    }
+}
+
+int main() {
+    test_pb_max_pattern();
+    test_pb_max_with_constraints();
+    return 0;
+}
\ No newline at end of file