Commit 17804fa
committed
Prefer actual constants to pseudo-constants in equivalence class machinery.
generate_base_implied_equalities_const() should prefer plain Consts over
other em_is_const eclass members when choosing the "pivot" value that
all the other members will be equated to. This makes it more likely that
the generated equalities will be useful in constraint-exclusion proofs.
Per report from Rushabh Lathia.1 parent 5a39114 commit 17804fa
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