A byte fuzzer pointed at a structured input spends most of its budget on inputs the decoder throws away. nelli mutates the typed choice sequence directly, so every mutant is valid by construction, and it uses a comparison log to defeat magic-value branches exactly.
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.
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.