Commit 36d4c09
fix(dispatch): restore cross-checking when GNN unavailable (CosineOnly mode)
Two bugs in verify_proof_cross_checked:
1. Early-return gated on CosineOnly — triggered permanently because the
GNN model is never loaded, silently preventing all cross-checks.
CosineOnly is about premise selection, not prover concurrency.
2. max_cross_checkers fell to 0 for CosineOnly via the _ => 0 arm,
so available_cross_checkers was always empty even after fixing (1).
3. cross_checked semantics: was `confirming_count >= 2` (≥2 provers
*proved* it) — should be `provers_used.len() >= 2` (we *ran* ≥2
provers for consistency). Unproved results are still cross-checked.
Fixes smoke_cross_check_z3_cvc5 (was failing since Phase 3 unblocked S4).
Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>1 parent 94002d0 commit 36d4c09
1 file changed
Lines changed: 14 additions & 9 deletions
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
721 | 721 | | |
722 | 722 | | |
723 | 723 | | |
724 | | - | |
| 724 | + | |
| 725 | + | |
| 726 | + | |
725 | 727 | | |
726 | 728 | | |
727 | | - | |
728 | | - | |
| 729 | + | |
729 | 730 | | |
730 | 731 | | |
731 | | - | |
| 732 | + | |
732 | 733 | | |
733 | 734 | | |
734 | 735 | | |
735 | 736 | | |
736 | | - | |
| 737 | + | |
737 | 738 | | |
738 | | - | |
| 739 | + | |
739 | 740 | | |
740 | 741 | | |
741 | 742 | | |
| |||
815 | 816 | | |
816 | 817 | | |
817 | 818 | | |
| 819 | + | |
| 820 | + | |
| 821 | + | |
| 822 | + | |
818 | 823 | | |
819 | 824 | | |
820 | 825 | | |
821 | | - | |
| 826 | + | |
822 | 827 | | |
823 | 828 | | |
824 | | - | |
| 829 | + | |
825 | 830 | | |
826 | | - | |
| 831 | + | |
827 | 832 | | |
828 | 833 | | |
829 | 834 | | |
| |||
0 commit comments