Symbolic-Execution

Sound integer abstraction in nelli's symbolic executor

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: one engine for property testing, fuzzing, and symbolic execution

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.