From 27fc564d09f8576600401d5931beb37740ea9def Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Mon, 2 Jul 2018 23:23:58 -0400 Subject: [PATCH] Remove bad assertion --- src/ast/proofs/proof_utils.h | 1 - 1 file changed, 1 deletion(-) 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