Skip to content

Commit

Permalink
comment
Browse files Browse the repository at this point in the history
  • Loading branch information
josef-widder committed May 29, 2024
1 parent ef697da commit 824b78a
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions specs/quint/specs/proofs-in-blocs/proofs.qnt
Original file line number Diff line number Diff line change
Expand Up @@ -105,13 +105,13 @@ def MaxEmptyWitness =
| None => true
}


// a proof with maximal empty blocks is added
def addMaximalProofWitness =
val s = strand(chain.last().height, numStrands)
val bs = strandBlocks(chain.slice(0, chain.length()-1), s, numStrands)
bs.emptySuffix().size() == maxMissingProofs implies
chain.last().proof == None


// Found an issue (7143ms).
// Use --seed=0xdc7a687c5dae7 to reproduce.
Expand Down

0 comments on commit 824b78a

Please sign in to comment.