diff --git a/lisa-utils/src/test/scala/lisa/test/ProofCheckerSuite.scala b/lisa-utils/src/test/scala/lisa/test/ProofCheckerSuite.scala index 6c3d6c4fe04861db76bbaee5963bdf54a716e503..4a989fa25d0b6d5bb6bdec5f1585ab99e0681f88 100644 --- a/lisa-utils/src/test/scala/lisa/test/ProofCheckerSuite.scala +++ b/lisa-utils/src/test/scala/lisa/test/ProofCheckerSuite.scala @@ -2,6 +2,8 @@ package lisa.test import lisa.kernel.proof.SCProof import lisa.kernel.proof.SCProofChecker.* +import lisa.kernel.proof.SCProofCheckerJudgement +import lisa.kernel.proof.SCProofCheckerJudgement.SCInvalidProof import lisa.kernel.proof.SequentCalculus.Sequent import lisa.kernel.proof.SequentCalculus.isSameSequent import lisa.utils.Helpers.{_, given} @@ -40,8 +42,7 @@ abstract class ProofCheckerSuite extends AnyFunSuite { def checkProof(proof: SCProof): Unit = { val judgement = checkSCProof(proof) - println(Printer.prettySCProof(judgement)) - println(s"\n(${proof.totalLength} proof steps in total)") + assert(judgement.isValid, Printer.prettySCProof(judgement, true)) } def checkProof(proof: SCProof, expected: Sequent): Unit = {