Z3

A symbolic executor has to encode every integer for the solver. Bit-vectors are correct but slow; unbounded integers are fast but unsound. nelli runs on bit-vectors and abstracts to unbounded integers only where it can prove the abstraction is safe. Measured, that is worth roughly 2 to 3x on range-bounded code and nothing on bit-twiddling. It also has a hole, which this post documents.

nelli is a Nim testing library built on a choice-sequence engine. Because a test input is just a recorded sequence of typed choices, the same engine drives property testing, coverage-guided fuzzing, and SMT-backed symbolic execution.