diff --git a/src/ast/ast.h b/src/ast/ast.h
index f081fc57f..15cd863fd 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -2368,6 +2368,12 @@ public:
     proof * mk_transitivity(proof * p1, proof * p2, proof * p3, proof * p4);
     proof * mk_transitivity(unsigned num_proofs, proof * const * proofs);
     proof * mk_transitivity(unsigned num_proofs, proof * const * proofs, expr * n1, expr * n2);
+    proof * mk_transitivity(std::initializer_list<proof*> const& proofs) {
+        return mk_transitivity(proofs.size(), proofs.begin());
+    }
+    proof * mk_transitivity(std::initializer_list<proof*> const& proofs, expr * n1, expr * n2) {
+        return mk_transitivity(proofs.size(), proofs.begin(), n1, n2);
+    }
     proof * mk_monotonicity(func_decl * R, app * f1, app * f2, unsigned num_proofs, proof * const * proofs);
     proof * mk_congruence(app * f1, app * f2, unsigned num_proofs, proof * const * proofs);
     proof * mk_oeq_congruence(app * f1, app * f2, unsigned num_proofs, proof * const * proofs);
@@ -2398,6 +2404,12 @@ public:
     proof * mk_def_axiom(expr * ax);
     proof * mk_unit_resolution(unsigned num_proofs, proof * const * proofs);
     proof * mk_unit_resolution(unsigned num_proofs, proof * const * proofs, expr * new_fact);
+    proof * mk_unit_resolution(std::initializer_list<proof*> const& proofs) {
+        return mk_unit_resolution(proofs.size(), proofs.begin());
+    }
+    proof * mk_unit_resolution(std::initializer_list<proof*> const& proofs, expr * new_fact) {
+        return mk_unit_resolution(proofs.size(), proofs.begin(), new_fact);
+    }
     proof * mk_hypothesis(expr * h);
     proof * mk_lemma(proof * p, expr * lemma);
 
diff --git a/src/smt/dyn_ack.cpp b/src/smt/dyn_ack.cpp
index 3779911cd..a2a96e8a4 100644
--- a/src/smt/dyn_ack.cpp
+++ b/src/smt/dyn_ack.cpp
@@ -89,8 +89,7 @@ namespace smt {
             app_ref eq(m.mk_eq(m_app1, m_app2), m);
             proof_ref a1(m.mk_congruence(m_app1, m_app2, prs.size(), prs.data()), m);
             proof_ref a2(mk_hypothesis(m, eq, true, m_app1, m_app2), m);
-            proof * antecedents[2] = { a1.get(), a2.get() };
-            proof_ref false_pr(m.mk_unit_resolution(2, antecedents), m);
+            proof_ref false_pr(m.mk_unit_resolution({ a1.get(), a2.get() }), m);
             lits.push_back(eq);
             SASSERT(lits.size() >= 2);
             app_ref lemma(m.mk_or(lits), m);
@@ -152,8 +151,7 @@ namespace smt {
             if (m.get_fact(p3) != m_eq3) p3 = m.mk_symmetry(p3);
             SASSERT(m.get_fact(p3) == m_eq3);
             p4 = m.mk_hypothesis(m.mk_not(m_eq3));
-            proof* ps[2] = { p3, p4 };
-            p5 = m.mk_unit_resolution(2, ps);
+            p5 = m.mk_unit_resolution({ p3, p4 });
             SASSERT(m.get_fact(p5) == m.mk_false());
             expr_ref conclusion(m.mk_or(m.mk_not(m_eq1), m.mk_not(m_eq2), m_eq3), m);
             p6 = m.mk_lemma(p5, conclusion);
diff --git a/src/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp
index a578b553d..0d81e8d9e 100644
--- a/src/smt/smt_conflict_resolution.cpp
+++ b/src/smt/smt_conflict_resolution.cpp
@@ -1333,9 +1333,8 @@ namespace smt {
         }
         else {
             pr = get_proof(consequent, conflict);
-            proof * prs[2] = { m_lit2proof[not_l], pr};
-            SASSERT(prs[0] && prs[1]);
-            pr = m.mk_unit_resolution(2, prs);
+            SASSERT(m_lit2proof[not_l] && pr);
+            pr = m.mk_unit_resolution({ m_lit2proof[not_l], pr });
         }
         expr_ref_buffer lits(m);
         for (literal lit : m_lemma) {
diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
index dce34a366..8889409c2 100644
--- a/src/smt/smt_internalizer.cpp
+++ b/src/smt/smt_internalizer.cpp
@@ -1656,8 +1656,7 @@ namespace smt {
                 proof * def = mk_clause_def_axiom(num_lits, lits, m.get_fact(pr));
                 TRACE(gate_clause, tout << mk_ll_pp(def, m) << "\n";
                       tout << mk_ll_pp(pr, m););
-                proof * prs[2] = { def, pr };
-                pr  = m.mk_unit_resolution(2, prs);
+                pr  = m.mk_unit_resolution({ def, pr });
             }
             mk_clause(num_lits, lits, mk_justification(justification_proof_wrapper(*this, pr)));
         }
diff --git a/src/tactic/goal.cpp b/src/tactic/goal.cpp
index 63d5e2ddc..a15298ac8 100644
--- a/src/tactic/goal.cpp
+++ b/src/tactic/goal.cpp
@@ -549,10 +549,8 @@ void goal::elim_redundancies() {
                 continue;
             if (pos_lits.is_marked(atom)) {
                 proof * p = nullptr;
-                if (proofs_enabled()) {
-                    proof * prs[2] = { pr(get_idx(atom)), pr(i) };
-                    p = m().mk_unit_resolution(2, prs);
-                }
+                if (proofs_enabled())
+                    p = m().mk_unit_resolution({ pr(get_idx(atom)), pr(i) });
                 expr_dependency_ref d(m());
                 if (unsat_core_enabled())
                     d = m().mk_join(dep(get_idx(atom)), dep(i));
@@ -566,10 +564,8 @@ void goal::elim_redundancies() {
                 continue;
             if (neg_lits.is_marked(f)) {
                 proof * p = nullptr;
-                if (proofs_enabled()) {
-                    proof * prs[2] = { pr(get_not_idx(f)), pr(i) };
-                    p = m().mk_unit_resolution(2, prs);
-                }
+                if (proofs_enabled())
+                    p = m().mk_unit_resolution({ pr(get_not_idx(f)), pr(i) });
                 expr_dependency_ref d(m());
                 if (unsat_core_enabled())
                     d = m().mk_join(dep(get_not_idx(f)), dep(i));
diff --git a/src/test/proof_checker.cpp b/src/test/proof_checker.cpp
index bc3dd39ad..ec5fc9edc 100644
--- a/src/test/proof_checker.cpp
+++ b/src/test/proof_checker.cpp
@@ -29,6 +29,52 @@ void tst_checker1() {
     VERIFY(checker.check(p4.get(), side_conditions));
 }
 
-void tst_proof_checker() {
-    tst_checker1();    
+void tst_initializer_list_overloads() {
+    ast_manager m(PGM_ENABLED);
+    expr_ref a(m), b(m);
+    proof_ref p1(m), p2(m), p3(m), p4(m);
+    expr_ref_vector side_conditions(m);
+
+    // Test mk_unit_resolution with initializer_list
+    a = m.mk_const(symbol("a"), m.mk_bool_sort());
+    b = m.mk_const(symbol("b"), m.mk_bool_sort());
+    p1 = m.mk_hypothesis(a.get());
+    p2 = m.mk_hypothesis(m.mk_not(a.get()));
+    
+    // Test the new initializer_list overload - should produce false
+    p3 = m.mk_unit_resolution({ p1.get(), p2.get() });
+    VERIFY(m.get_fact(p3.get()) == m.mk_false());
+    
+    // Test mk_unit_resolution with new_fact parameter
+    expr_ref fact(m.mk_or(a.get(), b.get()), m);
+    proof_ref pa_or_b(m.mk_hypothesis(fact.get()), m);
+    proof_ref pnot_a(m.mk_hypothesis(m.mk_not(a.get())), m);
+    p4 = m.mk_unit_resolution({ pa_or_b.get(), pnot_a.get() }, b.get());
+    VERIFY(m.get_fact(p4.get()) == b.get());
+    
+    // Test mk_transitivity with initializer_list
+    // Create a simple transitivity chain: a = b, b = c => a = c
+    expr_ref c(m);
+    c = m.mk_const(symbol("c"), m.mk_bool_sort());
+    
+    // Create rewrite proofs for a = b and b = c
+    proof_ref pr_ab(m.mk_rewrite(a.get(), b.get()), m);
+    proof_ref pr_bc(m.mk_rewrite(b.get(), c.get()), m);
+    
+    // Test the new initializer_list overload for transitivity
+    // This should create a proof of a = c
+    proof_ref p5(m.mk_transitivity({ pr_ab.get(), pr_bc.get() }), m);
+    VERIFY(p5.get() != nullptr);
+    // Verify the result is a proof with the expected fact (a = c)
+    expr* trans_fact = m.get_fact(p5.get());
+    VERIFY(m.is_eq(trans_fact));
+    VERIFY(to_app(trans_fact)->get_arg(0) == a.get());
+    VERIFY(to_app(trans_fact)->get_arg(1) == c.get());
+    
+    std::cout << "Initializer list overloads test passed!" << std::endl;
+}
+
+void tst_proof_checker() {
+    tst_checker1();
+    tst_initializer_list_overloads();
 }