Hard exhaustiveness instance in C#

test.cs

class Test {
    int f(int x0, int x1, int x2, int x3, int x4, int x5, int x6, int x7, int x8, int x9) {
        return (x0, x1, x2, x3, x4, x5, x6, x7, x8, x9) switch {
            (>= 78, >= 80, >= 83, >= 62, < 90, >= 32, < 84, < 77, >= 51, >= 8) => 0,
            (< 64, >= 85, >= 7, < 98, >= 71, < 26, >= 37, >= 34, < 5, < 39) => 1,
            (>= 23, >= 56, >= 36, >= 64, < 27, < 72, >= 67, >= 28, >= 93, >= 73) => 2,
            (>= 35, < 27, >= 71, >= 79, < 95, < 11, >= 86, < 32, < 32, >= 78) => 3,
            (< 86, >= 83, < 90, < 99, < 35, < 6, < 69, < 80, < 4, < 85) => 4,
            (< 38, >= 77, >= 70, >= 0, >= 9, < 96, < 5, < 39, >= 20, < 25) => 5,
            (< 46, >= 71, >= 74, < 2, < 79, < 56, >= 34, < 8, < 53, >= 36) => 6,
            (< 55, >= 99, >= 10, >= 6, < 36, < 2, < 22, < 29, < 0, >= 80) => 7,
            (< 16, < 43, < 79, < 68, >= 53, < 57, >= 35, < 21, < 98, < 15) => 8,
            (>= 90, < 62, < 60, >= 39, < 34, >= 40, < 23, < 42, < 92, >= 19) => 9,
            (>= 18, < 32, < 39, >= 94, < 89, < 95, < 70, >= 90, >= 28, < 58) => 10,
            (< 61, < 57, >= 95, < 4, >= 98, >= 34, >= 40, >= 59, < 55, >= 56) => 11,
            (>= 2, >= 34, < 5, < 58, < 19, < 44, < 95, >= 70, < 60, >= 17) => 12,
            (>= 89, < 49, < 42, < 23, < 39, < 3, >= 48, >= 65, < 48, < 64) => 13,
            (>= 15, >= 26, < 31, < 88, >= 58, < 35, < 4, < 84, >= 36, >= 71) => 14,
            (>= 91, >= 76, < 38, >= 46, < 74, < 55, < 19, >= 33, < 13, < 43) => 15,
            (< 85, < 72, < 77, < 60, < 57, < 75, < 25, < 37, >= 66, >= 0) => 16,
            (< 63, < 66, >= 49, < 5, < 46, >= 81, >= 6, < 69, >= 68, >= 99) => 17,
            (< 42, >= 10, < 97, >= 30, < 8, < 31, < 49, < 16, < 88, < 23) => 18,
            (< 69, < 89, >= 69, >= 16, >= 41, < 76, >= 43, >= 99, < 84, < 76) => 19,
            (< 97, >= 48, < 0, >= 18, >= 17, < 36, < 56, < 91, < 61, < 47) => 20,
            (< 58, >= 65, >= 40, < 48, < 87, < 46, < 74, < 48, >= 79, < 75) => 21,
            (< 27, < 29, < 52, >= 28, >= 31, >= 20, >= 54, < 10, < 70, >= 70) => 22,
            (< 31, < 61, < 75, >= 33, >= 84, < 66, >= 94, < 2, >= 65, < 72) => 23,
            (< 77, >= 64, >= 46, < 45, < 6, >= 79, >= 26, < 81, >= 94, >= 29) => 24,
            (>= 29, < 54, < 25, >= 27, < 15, >= 19, >= 17, >= 73, >= 8, < 69) => 25,
            (>= 26, < 88, >= 35, < 72, < 86, >= 89, >= 60, < 79, >= 81, >= 22) => 26,
            (>= 1, >= 47, < 19, < 63, >= 97, < 70, >= 89, >= 82, < 12, >= 63) => 27,
            (< 98, < 5, >= 22, < 40, >= 42, < 50, >= 12, >= 89, < 43, >= 9) => 28,
            (>= 30, < 74, < 37, < 11, >= 20, < 71, < 99, < 23, >= 83, >= 87) => 29,
            (>= 53, >= 67, < 93, >= 10, >= 1, >= 68, < 46, >= 49, < 34, < 74) => 30,
            (< 95, < 94, >= 94, >= 78, >= 61, < 12, >= 64, >= 27, >= 29, >= 93) => 31,
            (>= 3, < 90, >= 58, < 8, < 83, >= 45, < 63, >= 95, < 58, >= 28) => 32,
            (< 19, >= 98, >= 82, >= 57, >= 40, >= 94, >= 72, < 36, < 31, >= 49) => 33,
            (< 33, >= 40, < 98, < 31, >= 25, >= 47, < 9, < 78, >= 40, >= 66) => 34,
            (< 94, < 8, < 80, < 32, >= 7, < 86, >= 79, >= 53, < 89, >= 44) => 35,
            (>= 5, >= 22, < 6, >= 59, >= 78, >= 28, < 36, >= 22, < 33, >= 20) => 36,
            (>= 81, >= 41, < 84, < 67, < 11, < 85, >= 78, < 25, >= 50, >= 11) => 37,
            (>= 51, >= 46, < 15, >= 61, < 88, < 43, >= 3, < 30, < 14, < 55) => 38,
            (>= 17, >= 39, >= 3, < 29, >= 52, < 82, >= 20, >= 6, >= 47, >= 61) => 39,
            (>= 44, >= 1, < 91, < 95, >= 56, >= 93, >= 53, >= 60, < 73, < 65) => 40,
            (>= 10, < 73, < 78, >= 41, >= 29, >= 99, < 93, < 57, >= 99, >= 14) => 41,
            (>= 47, < 63, >= 67, >= 74, < 48, < 78, < 16, >= 44, >= 54, >= 88) => 42,
            (>= 41, >= 2, < 54, >= 12, >= 30, >= 49, < 52, >= 20, >= 85, < 5) => 43,
            (>= 40, < 79, >= 72, < 55, < 50, < 80, < 97, < 12, < 24, >= 48) => 44,
            (< 93, < 45, < 63, < 20, < 69, >= 9, < 7, >= 14, < 17, >= 57) => 45,
            (< 80, >= 21, >= 2, >= 86, < 91, >= 91, < 32, >= 76, < 44, >= 83) => 46,
            (>= 54, >= 16, >= 86, >= 43, >= 93, >= 88, >= 73, < 58, < 74, < 94) => 47,
            (< 37, >= 44, < 4, < 38, >= 68, < 69, < 77, < 96, < 2, >= 41) => 48,
            (< 92, >= 87, < 26, >= 93, >= 60, < 53, < 14, >= 18, >= 25, < 34) => 49,
            (>= 84, >= 7, < 27, < 24, >= 13, >= 16, >= 85, < 86, < 23, < 98) => 50,
            (>= 50, >= 78, >= 20, >= 15, < 66, < 4, < 58, < 4, < 78, < 90) => 51,
            (< 0, >= 58, >= 34, < 84, >= 16, < 23, < 88, >= 47, >= 18, >= 13) => 52,
            (>= 70, < 20, >= 48, >= 65, < 45, >= 13, >= 76, < 31, >= 30, < 4) => 53,
            (< 72, >= 13, < 12, >= 50, < 62, >= 51, < 10, < 97, < 86, < 81) => 54,
            (>= 39, >= 95, >= 88, >= 21, < 73, >= 64, >= 66, < 38, >= 67, < 35) => 55,
            (< 76, < 38, < 28, >= 89, < 38, < 67, < 80, < 19, >= 96, >= 46) => 56,
            (< 21, >= 14, >= 55, < 47, < 43, >= 14, >= 27, >= 66, >= 82, >= 33) => 57,
            (>= 43, < 11, < 85, < 42, >= 72, >= 24, >= 92, >= 41, >= 49, < 60) => 58,
            (>= 59, >= 23, < 11, >= 70, >= 21, < 0, < 2, < 85, >= 27, < 6) => 59,
            (>= 88, < 75, >= 9, < 80, < 51, >= 7, >= 33, >= 93, < 69, >= 7) => 60,
            (< 67, >= 15, >= 53, >= 97, < 92, >= 87, >= 18, < 9, < 75, >= 27) => 61,
            (>= 87, >= 25, < 73, < 56, < 37, >= 63, < 13, >= 92, >= 37, >= 91) => 62,
            (>= 36, >= 33, >= 24, < 19, >= 5, < 60, < 61, >= 40, < 39, < 31) => 63,
            (>= 20, < 84, >= 81, < 44, >= 67, >= 84, >= 41, < 17, >= 10, >= 97) => 64,
            (>= 79, < 18, < 17, < 69, < 18, < 73, >= 28, >= 51, >= 97, >= 92) => 65,
            (>= 11, >= 50, >= 45, < 25, < 44, < 59, < 62, >= 94, >= 87, < 2) => 66,
            (>= 57, < 36, >= 18, >= 85, < 49, >= 22, >= 68, >= 75, < 56, < 51) => 67,
            (>= 52, < 82, >= 41, < 35, >= 47, < 61, >= 57, >= 64, >= 16, >= 79) => 68,
            (< 49, >= 52, < 1, >= 73, >= 4, >= 21, < 55, >= 98, >= 21, >= 82) => 69,
            (>= 75, < 9, < 89, < 96, < 65, < 30, < 31, < 5, < 26, >= 26) => 70,
            (>= 60, < 30, >= 32, >= 26, < 23, >= 1, < 98, >= 13, >= 77, >= 30) => 71,
            (>= 13, >= 68, < 66, >= 92, < 10, >= 83, < 29, < 61, >= 1, >= 32) => 72,
            (>= 9, >= 96, >= 47, < 53, < 76, >= 33, < 75, >= 62, >= 95, >= 96) => 73,
            (< 12, >= 81, >= 68, >= 87, >= 94, < 98, < 21, >= 88, >= 42, >= 50) => 74,
            (>= 99, < 0, < 92, >= 37, >= 64, < 54, >= 59, >= 67, >= 19, >= 21) => 75,
            (>= 82, >= 59, >= 23, < 54, >= 32, >= 42, >= 51, >= 74, < 6, < 84) => 76,
            (< 6, >= 19, >= 96, < 22, >= 77, < 17, >= 83, >= 83, >= 15, < 24) => 77,
            (>= 4, < 4, < 33, < 91, < 85, >= 37, < 47, >= 68, < 45, >= 16) => 78,
            (< 7, < 3, < 16, >= 49, >= 99, >= 41, < 65, < 0, < 52, < 12) => 79,
            (< 74, >= 70, < 50, >= 90, >= 28, >= 65, >= 71, < 43, >= 62, >= 38) => 80,
            (< 73, < 31, >= 61, >= 71, >= 12, < 25, >= 87, >= 50, < 38, >= 86) => 81,
            (< 56, < 69, >= 99, < 1, < 54, < 38, >= 90, >= 52, >= 22, >= 37) => 82,
            (< 28, >= 55, >= 64, < 83, >= 55, < 10, < 50, >= 45, >= 9, >= 42) => 83,
            (< 14, >= 6, < 51, < 14, < 63, < 74, < 45, < 3, < 91, >= 95) => 84,
            (>= 8, < 93, >= 62, < 9, >= 75, >= 92, < 44, >= 63, >= 72, >= 53) => 85,
            (>= 62, < 91, < 29, < 76, >= 3, < 39, >= 30, >= 54, >= 64, < 89) => 86,
            (>= 34, >= 42, < 65, < 13, < 70, < 90, < 15, >= 15, < 46, >= 67) => 87,
            (>= 83, < 37, < 87, >= 81, < 26, < 97, < 82, >= 71, < 76, < 10) => 88,
            (< 96, < 35, < 56, < 77, < 0, < 8, < 81, >= 26, < 11, >= 18) => 89,
            (< 32, >= 97, >= 76, >= 51, >= 2, >= 15, < 42, < 55, < 7, < 45) => 90,
            (< 68, >= 60, >= 57, >= 36, >= 80, < 58, < 0, < 24, >= 57, < 40) => 91,
            (< 24, < 24, < 13, < 7, >= 22, >= 62, < 39, >= 1, < 90, < 62) => 92,
            (< 71, < 92, < 43, >= 82, >= 14, < 18, >= 24, < 72, >= 3, >= 59) => 93,
            (< 22, >= 17, < 8, < 52, >= 96, < 52, >= 1, >= 35, >= 71, >= 1) => 94,
            (>= 45, >= 86, >= 59, < 3, < 59, < 77, >= 38, >= 56, >= 35, < 77) => 95,
            (>= 25, >= 12, < 44, < 66, < 81, >= 5, >= 8, < 46, >= 63, < 52) => 96,
            (>= 66, >= 28, < 14, >= 17, < 82, >= 29, >= 96, >= 11, < 80, < 54) => 97,
            (< 48, < 53, >= 30, < 34, < 33, >= 27, >= 91, < 7, < 41, < 68) => 98,
            (>= 65, >= 51, >= 21, >= 75, >= 24, < 48, >= 11, >= 87, < 59, >= 3) => 99,
        };
    }
}

A switch of this form that has fewer than 2^10 cases could not be exhaustive.

Yes. It is easy to prove that this kind of switch is not exhaustive and state-of-the-art solvers will immediately see that.

In general, the ability to analyze this instance of the exhaustiveness checking problem highly depends on the algorithm that is being used. For example, any algorithm that tries to represent the non-covered state space in the form of disjoint hypercubes (e.g. by building a decision automata) is bound to take a very long time to solve this problem, since here the number of such hypercubes is very large (and, in the worst case, it grows exponentially with the size of the problem).

Apparently it does compile. See dotnet/roslyn#56230

warning CS8509: The switch expression does not handle all possible values of its input type (it is not exhaustive). For example, the pattern '(78, 80, 83, 62, 90, 0, _, _, _, _)' is not covered.

I was using sharplab.io to test it (which just hangs). I'll double-check with a recent command line-line compiler.

See dotnet/roslyn#56230 (comment) for a program that produces moderate-sized C# pattern-matching instances that are quite hard.

Thanks! Good one.