It occurred to me that the counterexample generated in the cex_with_repetition test could be shorter. While investigating, I found out this was because we forgot to propagate the states that correspond to "no repetitions" when checking for zero or more repetitions. This PR fixes this.
I also discovered that I wrote incorrect macro tests. Most notably, $( :: $ident )* is NOT a valid expression as far as expandable is concerned (0 repetitions means empty expansion, which is not a valid expression).
Obligatory meme:
It occurred to me that the counterexample generated in the
cex_with_repetitiontest could be shorter. While investigating, I found out this was because we forgot to propagate the states that correspond to "no repetitions" when checking for zero or more repetitions. This PR fixes this.I also discovered that I wrote incorrect macro tests. Most notably,
$( :: $ident )*is NOT a valid expression as far asexpandableis concerned (0 repetitions means empty expansion, which is not a valid expression).