fix(nondet-log): unsigned rows carried a duplicated value column

[GuilhermeBn198]

Found while reading nondet_log_to_file to plan H1.3 (per-input logs).

The defect

if  (type == UNSIGNED) fprintf(output, "%u;",  call->value.as_unsigned);
if  (type == DOUBLE)   fprintf(output, "%lf;", call->value.as_double);
else                   fprintf(output, "%d;",  call->value.as_int);

The first if has no else, so an UNSIGNED row falls through into the %d arm as well and prints its value twice. Reproduced against the installed binary before changing anything:

0;3;17;main;0;5;5;5      ← eight fields, where the format has seven

Why nothing caught it

It parses by accident. The value column is first, so it still lands at index 5 and readNonDetLog kept reading the right number — the emitted test suites were correct. What moved is the type column, to index 7, so any consumer of it reads a copy of the value instead.

And the live path is narrow: only __VERIFIER_nondet_unsigned reaches the UNSIGNED enumerator. __VERIFIER_nondet_uint is tagged UINT (13), a different enumerator, and always took the arm that was right. That is how it survived the entire v5/v6 baseline.

The fix

else if, plus two assertions where the format is actually produced — the CSV is written by the C runtime and nothing else in the repository checked its shape:

PASS every nondet log row has exactly 7 fields
PASS the type column survives as the last field (UNSIGNED=5)

They run in their own subdirectory: --debug keeps the scratch directory, and the cleanup assertion below them looks for exactly that at depth 1 of $WORK.

Verification

• Before: reproduced 0;3;17;main;0;5;5;5 (8 fields) with the already-installed binary — no rebuild, so this is the unmodified code.
• After: full build, emission suite 14/14.