- Notifications
You must be signed in to change notification settings - Fork28
Commit17804fa
committed
Prefer actual constants to pseudo-constants in equivalence class machinery.
generate_base_implied_equalities_const() should prefer plain Consts overother em_is_const eclass members when choosing the "pivot" value thatall the other members will be equated to. This makes it more likely thatthe generated equalities will be useful in constraint-exclusion proofs.Per report from Rushabh Lathia.1 parent5a39114 commit17804fa
1 file changed
+8
-2
lines changed| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
769 | 769 | | |
770 | 770 | | |
771 | 771 | | |
772 | | - | |
| 772 | + | |
| 773 | + | |
| 774 | + | |
| 775 | + | |
| 776 | + | |
| 777 | + | |
773 | 778 | | |
774 | 779 | | |
775 | 780 | | |
776 | 781 | | |
777 | 782 | | |
778 | 783 | | |
779 | 784 | | |
780 | | - | |
| 785 | + | |
| 786 | + | |
781 | 787 | | |
782 | 788 | | |
783 | 789 | | |
| |||
0 commit comments
Comments
(0)