diff --git a/src/test/proof_checker.cpp b/src/test/proof_checker.cpp
index bc3dd39ad..d600c60f5 100644
--- a/src/test/proof_checker.cpp
+++ b/src/test/proof_checker.cpp
@@ -29,6 +29,46 @@ 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
+    expr_ref c(m), eq_ab(m), eq_bc(m);
+    c = m.mk_const(symbol("c"), m.mk_bool_sort());
+    eq_ab = m.mk_eq(a.get(), b.get());
+    eq_bc = m.mk_eq(b.get(), c.get());
+    
+    proof_ref pr1(m.mk_reflexivity(eq_ab.get()), m);
+    proof_ref pr2(m.mk_reflexivity(eq_bc.get()), m);
+    
+    // Test the new initializer_list overload for transitivity
+    proof_ref p5(m.mk_transitivity({ pr1.get(), pr2.get() }), m);
+    VERIFY(p5.get() != nullptr);
+    
+    std::cout << "Initializer list overloads test passed!" << std::endl;
+}
+
+void tst_proof_checker() {
+    tst_checker1();
+    tst_initializer_list_overloads();
 }