fix(klee): name symbolic objects by their type, not by unexpanded macro text

[GuilhermeBn198]

Found while investigating H1.3 (per-input test vectors for Cover-Branches).

The defect

klee_make_symbolic(&non_det, sizeof(non_det), "non_det_#type");

#type inside a string literal is not the stringify operator — it is the two characters # and t. Every symbolic object in every .ktest was named the literal text non_det_#type: the same name for an int, a double and a char.

Why it survived every baseline

Nothing read that name. The nondet log carries its own type column, so suites were correct, verdicts were correct, and there was no symptom to notice — the classic shape of a bug that only becomes real when someone finally consumes the thing.

Why it matters now

KLEE writes one .ktest per explored path, each holding that path's input vector in consumption order:

test000001.ktest → [0, 0]
test000002.ktest → [42, 0]
test000003.ktest → [42, 7]   ← the violating vector

That is exactly the material a Cover-Branches suite is made of, produced by the engine for free and without perturbing the search. But a .ktest records each object's name, size and bytes — not its type, so the name is the only place a type can travel. Without it, four bytes could be an int, a float or half of a long, and nothing tells them apart.

	before	after
object 0	name: 'non_det_#type' size: 4	name: 'non_det_int' size: 4 int: 42
object 1	name: 'non_det_#type' size: 1	name: 'non_det_char' size: 1 int: 122

Test

tests/integration/test_ktest_object_names.sh, wired into the regression job. It asserts the pairing of name to size, not just the names — a one-byte object called non_det_int would be worse than no name at all.

PASS KLEE produced per-path test vectors (3)
PASS no object is named with the unexpanded macro text
PASS the int read is named non_det_int
PASS the char read is named non_det_char
PASS non_det_char is one byte, as its name promises

Writing it caught a trap worth recording in the test itself: klee-last is a symlink, and find does not descend into a symlinked start point without -L. The first version reported "no ktest files" on a run that had produced three.

Verification

Full build: new test 5/5, emission suite still 14/14 (the Cover-Error path is untouched).

Context: this replaces the H1.3 design I had started

I first implemented per-input vectors by having the C runtime write one log per terminating execution. The logic was right — 7/7 in an isolated native unit test — but the approach is not viable, and the measurement is unambiguous:

	wall clock	paths	verdict
collection off	1s	3 explored, 2 completed	FAILED ✅ correct
collection on	100s (budget exhausted)	—	SUCCEEDED ❌ wrong

One extra fopen per state under KLEE turns a one-second correct run into a timed-out wrong answer. That is corruption, not slowness, so none of it is in this PR. KLEE's own .ktest output gives the same vectors at no cost — which is what this fix unblocks.