Yes, correct. It does not and could not _actually_ run all possible executions unless the program state space is quite small. But from a user's perspective, it

Yes, correct. It does not and could not _actually_ run all possible executions unless the program state space is quite small. But from a user's perspective, it is similar. I have tried this pedagogical approach to describing verifiers like these as "infinite" unit tests before (to mixed results). It feels to me that what symbolic or constraint based reasoning (algebraic identities, programs, integrals, what have you) in general is doing is finding a way to finitely reason about a very large or actually infinite number of concretized cases.