Of course, one will attempt to also find equivalence classes for the states! The code

    long x = user_input();
    if (x == 0) {
        violate_model();
    } else {
        do_something();
    }

you would expect by any reasonable implementation to collapse the system into just two equivalent states that can be tested.

Ah, but finding equivalence classes of states is quite tricky! Obviously the naive approach of enumerating states and assigning them to equivalence classes is dead on arrival. You might be hinting at examining control flow predicates with your example. This technique is called predicate abstraction and underlies a lot of the SLAM effort. It works in certain scenarios - A statement which more or less captures the state of the field itself.

What I'm personally hinting at is symbolic/concolic execution. Essentially, each variable has a set of constraints associated with it - initially left blank for an input variable, for example. Then, the program can be executed, with assignments producing new constraints and replacing old ones. At each point in control flow, the executor chooses a path, and adds new constraints. When a dangerous statement (assertion, pointer dereference etc) is reached, the constraints can be solved by z3 or some other SMT solver, and if it can find a satisfying result you automatically have a test case that will produce erroneous or undefined behaviour.

It works quite well for short programs, actually - the KLEE people (or maybe it was DART) found bugs in busybox, GNU Coreutils etc.

The current approach is to instead of traversing your control flow tree explicitly (which means you're doing a tree search over a potentially infinite tree), converting the program such that it produces a logical statement that can be solved by an SMT solver, that is satisfiable iff there is an input that leads to a bug within that bounded number of loop unwindings.

With fun C++ metaprogramming, you can actually get this to happen natively (i.e. the parts that aren't reliant on input get run natively) which leads to a massive speedup o

I don't believe it to be model checking, although it might use model checking techniques. I could be wrong, I'm only familiar with a few aspects.