{
  "target": "./weak",
  "results": [
    {
      "lemma": "scan_bounds",
      "verdict": "PROVED",
      "solver": "z3",
      "duration_ms": 11,
      "file": "weak/scan.go",
      "line": 8,
      "smtlib_query": "; reqproof verify-lemma — Phase E orchestrator\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_bounds ((items (Seq Int))) Bool (let ((result (FirstNegative items))) (and (\u003c= 0 result) (\u003c= result (seq.len items)))))\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 (\u003c= 0 i$2) (\u003c= i$2 (seq.len items))))))) (forall ((items (Seq Int)) (i Int)) (=\u003e (and (and (\u003c= 0 i) (\u003c= i (seq.len items))) (and (\u003c i (seq.len items)) (\u003e= (seq.nth items i) 0))) (let ((i$1 (+ i 1))) (and (\u003c= 0 i$1) (\u003c= i$1 (seq.len items))))))) (forall ((items (Seq Int)) (i Int)) (=\u003e (and (\u003c= 0 i) (\u003c= i (seq.len items))) (and (\u003c= 0 (FirstNegative_loop_0 items i)) (\u003c= (FirstNegative_loop_0 items i) (seq.len 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 (\u003c= 0 i$2) (\u003c= i$2 (seq.len items))))))) (forall ((items (Seq Int)) (i Int)) (=\u003e (and (and (\u003c= 0 i) (\u003c= i (seq.len items))) (and (\u003c i (seq.len items)) (\u003e= (seq.nth items i) 0))) (let ((i$1 (+ i 1))) (and (\u003c= 0 i$1) (\u003c= i$1 (seq.len items)))))) (proof_scan_bounds items))))\n(check-sat)\n(get-model)\n"
    }
  ],
  "stats": {
    "total": 1,
    "proved": 1,
    "counterexample": 0,
    "timeout": 0,
    "unknown": 0,
    "translation_error": 0,
    "all_proved": true
  }
}