The following rule matched way too many comparisons, which were transformed by the requires clause into two parallel comparisons and a #distinctBits(VAL1, VAL2) term that would never evaluate to true. The better solution is to match the terms in the main rule, not in #distinctBits, even if that makes the rule a bit uglier.
rule VAL1 +Int VAL2 <Int MAX => true requires VAL1 <Int MAX andBool VAL2 <Int MAX andBool #distinctBits(VAL1, VAL2) [simplification]
Preliminary tests show that this PR likely fixes the main Coindrip performance problems.
The following rule matched way too many comparisons, which were transformed by the
requiresclause into two parallel comparisons and a#distinctBits(VAL1, VAL2)term that would never evaluate to true. The better solution is to match the terms in the main rule, not in#distinctBits, even if that makes the rule a bit uglier.Preliminary tests show that this PR likely fixes the main Coindrip performance problems.