// Optional KLEE confirmation fixture for Fold's future DAST lane.
// Build/run with tests/confirmation/klee/run_klee_smoke.sh when KLEE is installed.
#include <stddef.h>

#ifdef KLEE
#include <klee/klee.h>
#endif

int vulnerable_copy(unsigned idx) {
    char buf[8] = {0};
    if (idx >= 16)
        return 0;
    buf[idx] = 'X'; // idx in [8,15] is an out-of-bounds write.
    return buf[0];
}

int main(void) {
    unsigned idx = 0;
#ifdef KLEE
    klee_make_symbolic(&idx, sizeof(idx), "idx");
#else
    idx = 9;
#endif
    return vulnerable_copy(idx);
}