UNKNOWN / TIMEOUT log annotation protocol v4.2 — v4.1 anchor corrections applied

v4.2 changes (3件): TIMEOUT-2: Evidence explicit → indirect（ログに "TIMEOUT" 文字列不在） |  Config-Coverage-1: Using default analysis アンカー削除（ログ不在） |  Plain-Unknown-1: Using default analysis アンカー削除（ログ不在）

Annotation protocol — column rules

Surface — verdict string verbatim, no paraphrase.
Evidence — explicit: log contains a direct statement supporting the terminal cause. indirect: inferred from pattern or absence.
Terminal cause (pick exactly 1) — Resource · Config-Missing · Unsupported · Incomplete
Diagnostic cause (max 2 from fixed list) — search-space · config-absent · property-unsupported · precision-loss · fallback-failed · unobservable
Confidence — safe: log states it directly · plausible: one inference step · risky: multi-step or ambiguous
Run validity — unsupported · incomplete · questionable · valid

Boundary rule — observed: filled from log text alone, no "because". interpreted: requires at least one "because X → Y" step.

ID / Pattern observed (log-literal) interpreted (inference)
Surface Evidence Raw-log anchors Terminal cause Diagnostic cause Confidence Run validity
TIMEOUT-1
P-RESOURCE		 TIMEOUT / ERROR
(SIGNAL 15)		 indirect
PORTFOLIO :: {'program': 'Program', 'spec': 'Specification'} Verifier :: esbmc-kind Verifier :: utaipan Verifier :: two_ls Verifier :: symbiotic {'verdict': 'ERROR(SIGNAL 15)', 'witness': }
Resource unobservable

SIGTERM in log; which verifier was running and at what state is not exposed.

 plausible incomplete
TIMEOUT-2
P-RESOURCE
v4.2 updated 		TIMEOUT indirect
Partial Incremental Mode 153 variables, 66 clauses SAT checker: instance is SATISFIABLE SAT checker inconsistent: instance is UNSATISFIABLE 75723 variables, 15605 clauses 75724 variables, 12 clauses

⚠ "TIMEOUT" 文字列はログ内に存在しない。ログがSAT繰り返し後に途切れることから外部killを推定。Evidence を explicit → indirect に修正。

 Resource search-space

Variable counts are in log (153→75723). "search-space" is one inference step from those counts.

 plausible incomplete
TIMEOUT-3
P-RESOURCE
v4.1 updated 		TIMEOUT indirect
INFO: Starting verification klee -dump-states-on-halt=0 ... -max-time=0 KLEE: output directory is "…/klee-out-0" KLEE: Using Z3 solver backend [log ends here — no further output]

⚠ v3 anchors Tool 'klee' reached timeout 2s and KLEE: ctrl-c detected not present in this log. Removed.

 Resource unobservable

-max-time=0 = no internal KLEE timeout. Log truncates immediately after Z3 init. External kill inferred.

 plausible incomplete
Config-Coverage-1
P-CONFIG
v4.2 updated 		UNKNOWN / ERROR explicit
Ultimate.py --spec …/termination.prp No suitable file found in config dir using search string *Termination.xml No suitable toolchain file found using *Termination.xml

⚠ Using default analysis はログに存在しない。削除。

 Config-Missing config-absent

Search string and failure both in log. No inference step required.

 safe unsupported
Config-Coverage-2
P-CHAIN		 UNKNOWN explicit
TerminationAnalysisResult: Unable to decide termination Overapproximations C: (x-1)&y [17] (Reason bitwiseAnd) RESULT: unable to determine termination Using bit-precise analysis No suitable settings file found using Termination*64bit*_Bitvector ERROR: UNSUPPORTED PROPERTY Result: UNKNOWN
Incomplete → Config-Missing

Two distinct terminal events chained.

 precision-loss fallback-failed

Log transition (chain)

① Unable to decide + Reason bitwiseAnd → precision-loss
↓ fallback triggered
② Using bit-precise analysis → attempt noted in log
↓ config lookup
③ No suitable settings file …Bitvector → fallback-failed

Each anchor individually explicit; connecting ①→②→③ requires knowing the fallback mechanism.

 plausible incomplete
Config-Coverage-3
P-UNSUP		 UNKNOWN / ERROR explicit
Bubaak version 0.9.2 - program terminates does not support termination Caught exception, killing tasks... NotImplementedError("BSELF does not support termination")
Unsupported property-unsupported

Exception text is in log verbatim. No inference required.

 safe unsupported
Plain-Unknown-1
P-CONFIG
v4.2 updated 		UNKNOWN / ERROR explicit
Ultimate.py --spec …/termination.prp and-03-false.c No suitable file found in config dir using search string *Termination.xml No suitable toolchain file found using *Termination.xml

⚠ Using default analysis はログに存在しない。削除。

 Config-Missing config-absent

Same pattern as CC-1. Search and failure both in log.

 safe unsupported
Plain-Unknown-2
P-INCOMPLETE		 UNKNOWN /
INCOMPLETE		 explicit
Counterexample to termination found, but deemed imprecise Termination algorithm did not find a non-terminating loop. Analysis 2 terminated, but result is unsound. No further configuration available. Verification result: UNKNOWN, incomplete analysis.
Incomplete precision-loss

"Imprecise" and "unsound" are in log. What caused the imprecision is not stated — identifying the primary factor is the risky step.

 risky questionable
Plain-Unknown-3
P-INCOMPLETE		 UNKNOWN indirect
Specification: Termination → enabling termination analyses unrolling loop at …and-04-false.c:15 with factor 12 SV-COMP specification: CHECK( init(main()), LTL(F end) ) [Warning][Integer > Overflow][CWE-191] Signed integer underflow [Warning][Termination] The program might not terminate! [Warning][Deadcode][CWE-571] condition 'x < 8' always true SV-COMP result: unknown
Incomplete precision-loss

Warning cluster is in log. Causal link to UNKNOWN is inferred.

 risky valid
3
safe confidence
CC-1, CC-3, PU-1
4
plausible confidence
T-1, T-2, T-3, CC-2
2
risky confidence
PU-2, PU-3
3
indirect evidence
T-1, T-2, T-3

v4.2 changes: TIMEOUT-2 evidence corrected to indirect (no "TIMEOUT" string in log; log truncates after SAT loop). Config-Coverage-1 and Plain-Unknown-1: phantom anchor Using default analysis removed (absent from both logs).
v4.1 change (retained): TIMEOUT-3 anchors corrected from actual log. Two phantom anchors removed. -max-time=0 added as the log-literal explanation for absent KLEE timeout message.