diff --git a/src/ast/proofs/proof_utils.h b/src/ast/proofs/proof_utils.h
index 1fd6eb449..e3ad8d06e 100644
--- a/src/ast/proofs/proof_utils.h
+++ b/src/ast/proofs/proof_utils.h
@@ -202,7 +202,6 @@ public:
                 }
                 else {
                     // rebuild unit resolution
-                    SASSERT(parents.size() == args.size() - 1);
                     newp = m.mk_unit_resolution(parents.size(), parents.c_ptr());
                     // XXX the old and new facts should be
                     // equivalent. The test here is much