{
  "target": "./baseline",
  "results": [
    {
      "lemma": "scan_contract",
      "verdict": "TIMEOUT",
      "solver": "z3",
      "duration_ms": 15012,
      "file": "baseline/scan.go",
      "line": 8,
      "smtlib_query": "; reqproof verify-lemma — Phase E orchestrator\n(define-fun-rec PrefixOK ((end Int) (items (Seq Int))) Bool (ite (\u003c= end 0) true (and (\u003e= (seq.nth items (- end 1)) 0) (PrefixOK (- end 1) items))))\n(define-fun-rec FirstNegative_loop_0 ((items (Seq Int)) (i Int)) Int\n  (ite (and (\u003c i (seq.len items)) (\u003e= (seq.nth items i) 0))\n    (let ((i$1 (+ i 1))) (FirstNegative_loop_0 items i$1))\n    i))\n(define-fun FirstNegative ((items (Seq Int))) Int (let ((i 0)) (let ((i$1 1)) (let ((i$2 (ite (\u003e (seq.len items) 0) i$1 i))) (FirstNegative_loop_0 items i$2)))))\n(define-fun proof_scan_contract ((items (Seq Int))) Bool (let ((result (FirstNegative items))) (and (and (and (\u003c= 0 result) (\u003c= result (seq.len items))) (PrefixOK result items)) (or (= result (seq.len items)) (\u003c (seq.nth items result) 0)))))\n(declare-fun items () (Seq Int))\n(assert (=\u003e (and (forall ((items (Seq Int))) (let ((i 0)) (let ((i$1 1)) (let ((i$2 (ite (\u003e (seq.len items) 0) i$1 i))) (and (and (\u003c= 0 i$2) (\u003c= i$2 (seq.len items))) (PrefixOK i$2 items)))))) (forall ((items (Seq Int)) (i Int)) (=\u003e (and (and (and (\u003c= 0 i) (\u003c= i (seq.len items))) (PrefixOK i items)) (and (\u003c i (seq.len items)) (\u003e= (seq.nth items i) 0))) (let ((i$1 (+ i 1))) (and (and (\u003c= 0 i$1) (\u003c= i$1 (seq.len items))) (PrefixOK i$1 items)))))) (forall ((items (Seq Int)) (i Int)) (=\u003e (and (and (\u003c= 0 i) (\u003c= i (seq.len items))) (PrefixOK i items)) (and (and (\u003c= 0 (FirstNegative_loop_0 items i)) (\u003c= (FirstNegative_loop_0 items i) (seq.len items))) (PrefixOK (FirstNegative_loop_0 items i) items))))))\n(assert (and (\u003c= 0 (seq.len items)) (\u003c= (seq.len items) 32)))\n(assert (not (and (forall ((items (Seq Int))) (let ((i 0)) (let ((i$1 1)) (let ((i$2 (ite (\u003e (seq.len items) 0) i$1 i))) (and (and (\u003c= 0 i$2) (\u003c= i$2 (seq.len items))) (PrefixOK i$2 items)))))) (forall ((items (Seq Int)) (i Int)) (=\u003e (and (and (and (\u003c= 0 i) (\u003c= i (seq.len items))) (PrefixOK i items)) (and (\u003c i (seq.len items)) (\u003e= (seq.nth items i) 0))) (let ((i$1 (+ i 1))) (and (and (\u003c= 0 i$1) (\u003c= i$1 (seq.len items))) (PrefixOK i$1 items))))) (proof_scan_contract items))))\n(check-sat)\n(get-model)\n"
    }
  ],
  "stats": {
    "total": 1,
    "proved": 0,
    "counterexample": 0,
    "timeout": 1,
    "unknown": 0,
    "translation_error": 0,
    "all_proved": false
  }
}