diff --git a/specs/quint/specs/proofs-in-blocs/proofs.qnt b/specs/quint/specs/proofs-in-blocs/proofs.qnt index 37f723b7c..3a6530df6 100644 --- a/specs/quint/specs/proofs-in-blocs/proofs.qnt +++ b/specs/quint/specs/proofs-in-blocs/proofs.qnt @@ -82,7 +82,7 @@ var num_unproven_blocks: StrandInfo // If a block contains transactions then it is at the very beginning, or the block also contains a proof -def transactionNeedsProofInv = +def payloadImpliesProofInv = chain.last().txs implies chain.last().height < numStrands or chain.last().proof != None // The number of proofs of empty blocks in a recursive proof is bounded by maxMissingProofs