NITWIT 4

NITWIT validates violation witnesses of C programs, as in SV-COMP: it executes the program with an interpreter, follows the witness, and searches for input values where the witness needs them. A witness is confirmed only by one complete run in which every waypoint had its outcome. NITWIT 4 is written in C++23: a C front end produces a typed AST, an interpreter executes it with a precise memory model, and the validation layer observes the execution. It replaces NITWIT 3.x (branch old) and keeps its command line and exit codes, with the differences listed in docs/release.md and docs/exit-codes.md.

Quick start

On Linux with GCC 14, CMake and Ninja (docs/development.md), from the root of the repository:

cmake --preset gcc-release && cmake --build --preset gcc-release
~/nitwit-build$PWD/gcc-release/src/driver/nitwit -64 -w witness.yml -p unreach-call.prp program.c
ctest --preset gcc-release            # the tests
tools/package.sh                      # the release archive for BenchExec and fm-tools (docs/release.md)

The last line of the output is the result (VALIDATED:, FAILED:, UNKNOWN: or ERROR:), and the exit code says the same to BenchExec (docs/exit-codes.md). With --write-witness concrete.yml, a confirmed witness is also written as a concrete witness that gives every input of the confirming run, and --strict-inputs validates a witness only on the inputs it gives (src/validate/README.md, "Concrete witnesses" and "Strict inputs").

What NITWIT supports

• Property: unreach-call. Any other property gives UNKNOWN (exit 4).
• Witnesses: violation witnesses in format 2.x (YAML; SV-COMP 2026 uses 2.0 and 2.1). Witnesses with cycle waypoints or a thread_id other than 0 give UNKNOWN, and so do witnesses in format 1.0 (GraphML). Correctness witnesses in format 2.x are refuted where a run of the program, which follows no witness, calls the error function (REFUTED:, exit 253), and are UNKNOWN otherwise: NITWIT reads none of their invariants and never confirms one (src/validate/README.md, "Correctness witnesses").
• Data models: ILP32 (-32, the default) and LP64 (-64), with the types, layouts and arithmetic of GCC on i386 and x86-64.
• C: C17 with the GNU extensions that sv-benchmarks uses (src/parse/README.md), pre-C99 code (implicit int, K&R definitions, implicit declarations), and the C library functions of sv-benchmarks with glibc's behaviour (src/interp/README.md). Files with preprocessor directives other than line markers, #line, #ident, #pragma and the null directive go through the system cpp.
• Not supported (UNKNOWN), the main items: threads, inline assembly other than an empty template, files, signals, atexit, the scanf family, computed goto, nested functions, arithmetic on _Complex values, and a longjmp to a setjmp that is not one of the uses C11 allows or the value assigned to a variable (src/interp/README.md, "Non-local jumps"). __float128 is computed as long double. The module READMEs list the rest (src/lex/README.md, src/parse/README.md, src/sema/README.md, src/interp/README.md, src/validate/README.md).

Results

NITWIT 4 (the release archive built from 0914f93, and from b146595, which supports setjmp and longjmp, for the 373 witnesses whose programs name them) on the 27,767 unreach-call witnesses of SV-COMP 2026 in format 2.x, at SV-COMP's 90 s: it confirms 9,526 of the 14,841 witnesses of buggy programs (64 %) and none of the 12,792 witnesses of correct programs. On the 11,738 witnesses of buggy programs that the SV-COMP 2026 validators ran on, it confirms 7,054, more than any of them alone (the best, Witch, 5,392), and unlike CPAchecker and MetaVal it confirms no witness of a correct program. On 1000 of the witnesses (100 per producer), it confirms 601 of the 851 witnesses of buggy programs, NITWIT 3.x 312; on the witnesses both decide, it takes 15 s of CPU time, 3.x 348 s. The path search between waypoints and the copies of uninitialized bytes (after 4.2.0) confirm 66 more witnesses of buggy programs and none of correct programs on the runs that ended within 90 s, and refute 617 of 3,204 buggy programs' correctness witnesses (4.2.0: 415). Details, also on memory: docs/evaluation.md.

The test suites (docs/development.md, "Tests"): unit tests, golden dumps and semantics with this source, the validation of witnesses with the build above:

Suite	Result
unit tests	2,031 tests of the 10 modules, all passing
golden dumps	48: 22 ASTs; 26 typed ASTs, 4 of them for ILP32; all passing
semantics	51 programs with the output, outcome and inputs of GCC and Clang, with -m32 and -m64, also with the terms checked: 204 tests, all passing
validation of all SV-COMP 2026 unreach-call witnesses (format 2.x)	the front end accepts every program; all witnesses but one (line: 0) parse; 9,526 of 14,841 witnesses of buggy programs confirmed, none of 12,792 of correct programs
validation-crafted	96 of 100 right, no invalid witness confirmed; 100 of 100 with the path search
testfiles/	all 45 format 2.x witnesses right
release	nitwit.sh and the smoke test of the archive pass; so does fm-weck's smoke test in fm-tools' CI (Ubuntu 26.04, container mode, the SV-COMP 2027 image)

Documentation

• docs/architecture.md: goals, modules and key design decisions
• docs/guidelines.md: coding guidelines and review checklist
• docs/development.md: toolchain, building, tests, contributing
• docs/exit-codes.md: exit codes (compatible with NITWIT 3.x)
• docs/release.md: the release archive for BenchExec and fm-tools, and how to release
• docs/evaluation.md: NITWIT 4.0 on all SV-COMP 2026 unreach-call witnesses, against 3.x and the other SV-COMP validators
• docs/roadmap.md: open work
• the module READMEs in src/<module>/README.md: semantics, rules and known gaps of each module
• tools/difftest/README.md: differential testing against GCC and Clang
• release/README.md and release/THIRD-PARTY.md: the README and the third-party notices of the release archive
• LICENSE: NITWIT 4 is licensed under the New BSD license (BSD-3-Clause)