LemmaNoDuplicatesInConcat would fail with certain random seeds, especially with newer Z3 versions. This change proves the result in smaller pieces rather than all in one go. It's arguably more readable, too.
LemmaFlattenLengthLeMul and LemmaFilterDistributesOverConcat also sometimes timed out or failed, but a few instances of {:split_here} seem to solve those issues.
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.
LemmaNoDuplicatesInConcat would fail with certain random seeds, especially with newer Z3 versions. This change proves the result in smaller pieces rather than all in one go. It's arguably more readable, too.
LemmaFlattenLengthLeMul and LemmaFilterDistributesOverConcat also sometimes timed out or failed, but a few instances of
{:split_here}seem to solve those issues.By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.