diff --git a/bench/policy-compliance-fixtures/README.md b/bench/policy-compliance-fixtures/README.md
new file mode 100644
index 0000000..0e7c39e
--- /dev/null
+++ b/bench/policy-compliance-fixtures/README.md
@@ -0,0 +1,153 @@
+# policy-compliance-fixtures
+
+Six policy-compliance verification tasks that serve as the shared input corpus
+for the Milestone 3 comparative analysis in `bench/symbolic-comparison.md`
+(parent issue: `bench/symbolic-comparison.md`). Each task describes a single
+authorization / resource-access / data-protection policy together with:
+
+- its **policy rules** (the declarative invariant the verifier must enforce),
+- its **known paths / branches** (the reachable verdict branches, each with a
+  concrete witness input that exercises it),
+- a **concrete representation** (a CEL boolean expression runnable today via
+  `POST /v1/verify/criterion` with `verify_method: "cel_expr"`), and
+- a **symbolic representation** (an SMT-LIB2 formula runnable today via
+  `POST /v1/verify/z3`, and the future symbolic-execution engine).
+
+The two representations express the *same* allow-path condition so that
+concrete testing and symbolic execution can be compared apples-to-apples on
+path coverage and constraint-solving time.
+
+This sub-issue only ships the fixtures. Running both engines over them and
+writing the comparison document is the parent issue's job.
+
+## Fixture set
+
+The six tasks are ordered by increasing structural complexity, spanning the
+range required by the acceptance criteria (simple condition → complex nested
+policy):
+
+| # | File | Domain | Complexity | Branches | Construct introduced |
+|---|------|--------|------------|----------|-----------------------|
+| 1 | [`auth-minimum-age.json`](auth-minimum-age.json)         | authorization | simple    | 2 | single relational condition |
+| 2 | [`rbac-role-check.json`](rbac-role-check.json)           | authorization | simple    | 3 | disjunction / set membership |
+| 3 | [`resource-quota.json`](resource-quota.json)             | resource-access | moderate | 2 | linear arithmetic over 3 vars |
+| 4 | [`time-window-access.json`](time-window-access.json)     | resource-access | moderate | 3 | nested conjunction of bounds |
+| 5 | [`tiered-rate-limit.json`](tiered-rate-limit.json)       | resource-access | complex  | 3 | mixed disjunction + conjunction |
+| 6 | [`data-residency-geo.json`](data-residency-geo.json)     | data-protection | complex  | 4 | conjunctive predicate set + negated membership |
+
+Every task carries a `complexity` field; together they cover simple
+conditions, moderate constraints, and complex nested policies.
+
+## Per-task summary
+
+### 1. `auth-minimum-age` — Minimum-age authorization gate (simple)
+**Policy.** Principal age MUST be >= 18.
+**Paths.** `allow` (`age >= 18`, witness `age=18`) · `deny` (`age < 18`, witness `age=12`).
+**CEL.** `age >= 18`  ·  **SMT.** `(assert (>= age 18))` → `sat`.
+**Expected behavior.** Boundary `age == 18` is allowed (closed lower bound); both branches are independently feasible.
+
+### 2. `rbac-role-check` — Role-based access control (simple, disjunctive)
+**Policy.** Role MUST be in `{admin, editor}`.
+**Paths.** `allow-admin` (`admin`) · `allow-editor` (`editor`) · `deny-other` (witness `viewer`).
+**CEL.** `role == "admin" || role == "editor"`  ·  **SMT.** `(assert (or (= role 1) (= role 2)))` → `sat` (role codes admin=1, editor=2).
+**Expected behavior.** Three feasible paths: one per allow-set member plus default deny.
+
+### 3. `resource-quota` — Capacity-arithmetic gate (moderate)
+**Policy.** `used + requested <= limit`.
+**Paths.** `allow-within-quota` (witness `used=30,requested=20,limit=100`) · `deny-over-quota` (witness `used=90,requested=20,limit=100`).
+**CEL.** `used + requested <= limit`  ·  **SMT.** `(assert (<= (+ used requested) limit))` → `sat`.
+**Expected behavior.** Boundary (`used + requested == limit`) is allowed; tests additive capacity reasoning rather than equality.
+
+### 4. `time-window-access` — Business-hours window (moderate, nested)
+**Policy.** `9 <= hour <= 17` AND `1 <= day <= 5` (Mon–Fri).
+**Paths.** `allow-business-hours` (witness `hour=12,day=3`) · `deny-off-hours` (witness `hour=23,day=3`) · `deny-weekend` (witness `hour=12,day=7`).
+**CEL.** `hour >= 9 && hour <= 17 && day >= 1 && day <= 5`  ·  **SMT.** conjunction of four bounds → `sat`.
+**Expected behavior.** Two independent ranged predicates; each fails on its own sub-path. `day` is 1..7 (1=Mon…7=Sun).
+
+### 5. `tiered-rate-limit` — Tiered limit with burst (complex, mixed)
+**Policy.** `request_count <= 100` OR (`request_count <= 200` AND `tier == "premium"`).
+**Paths.** `allow-under-base` (witness `count=50,tier=free`) · `allow-premium-burst` (witness `count=150,tier=premium`) · `deny-over-limit` (witness `count=250,tier=premium`).
+**CEL.** `request_count <= 100 || (request_count <= 200 && tier == "premium")`  ·  **SMT.** mixed disjunction/conjunction → `sat` (tier code premium=1).
+**Expected behavior.** The burst path is reachable only through the nested conjunction; richest branching in the set.
+
+### 6. `data-residency-geo` — Geo-fencing compliance (complex, conjunctive)
+**Policy.** `region == "EU"` AND `country` NOT in `{"X","Y"}` AND `encrypted == true`.
+**Paths.** `allow-compliant` · `deny-wrong-region` · `deny-blocked-country` · `deny-unencrypted` (witnesses in the file).
+**CEL.** `region == "EU" && !(country in ["X", "Y"]) && encrypted == true`  ·  **SMT.** conjunction of equality + two negated equalities + boolean → `sat` (region EU=1; blocked X=10, Y=11).
+**Expected behavior.** Most predicate-dense policy; three independent deny sub-paths plus one allow path.
+
+## File format
+
+Each `<task-id>.json` is a self-contained task with this shape:
+
+```jsonc
+{
+  "id": "auth-minimum-age",            // stable identifier, matches file stem
+  "title": "...",
+  "category": "authorization",          // authorization | resource-access | data-protection
+  "complexity": "simple",               // simple | moderate | complex
+  "description": "...",                 // prose: what the policy enforces and why
+  "policy_rules": ["..."],              // declarative rules the verifier must enforce
+  "expected_behavior": "...",           // allow/deny semantics + boundary behaviour
+  "paths": [                            // reachable verdict branches (path coverage map)
+    { "id": "allow", "condition": "...", "verdict": "allow"|"deny",
+      "feasible": true, "witness": { "...": ... } }
+  ],
+  "representations": {
+    "cel":  { "endpoint": "POST /v1/verify/criterion", "verify_method": "cel_expr",
+              "expr": "...", "context_template": { "...": ... } },
+    "smt2": { "endpoint": "POST /v1/verify/z3",
+              "declarations": "(declare-const ...)", "policy_assertion": "(assert ...)",
+              "expected_check_sat": "sat", "notes": "..." }
+  },
+  "samples": [                          // concrete inputs + expected verdicts (golden cases)
+    { "name": "...", "context": { "...": ... }, "expected_cel": true, "expected_path": "allow" }
+  ]
+}
+```
+
+`paths[].witness` and `samples[].context` are concrete inputs that exercise a
+specific branch; the symbolic explorer uses the `paths` to enumerate coverage
+while the concrete tester uses `samples` (and the CEL `expr`) as golden cases.
+
+## Running the fixtures
+
+### Concrete testing (CEL — available today)
+
+POST a task's CEL representation to the criterion endpoint:
+
+```bash
+curl -s localhost:8080/v1/verify/criterion -d '{
+  "criterion": {
+    "id": "auth-minimum-age",
+    "verify_method": "cel_expr",
+    "arg": {"expr": "age >= 18", "context": {"age": 25}},
+    "level": "hard", "category": "security"
+  }
+}'
+# => {"ok":true,"criterionId":"auth-minimum-age"}
+```
+
+`bench/policy_compliance_fixtures_test.go` automates this: it loads every
+`*.json` in this directory, then runs each task's CEL `expr` against every
+`samples[].context` through the real `internal/cel` evaluator and asserts the
+result equals `samples[].expected_cel`. This is the concrete-testing
+acceptance criterion, pinned so it cannot silently regress.
+
+### Symbolic execution (SMT-LIB2 — available today via Z3; full engine pending)
+
+POST a task's SMT-LIB2 to the Z3 endpoint:
+
+```bash
+curl -s localhost:8080/v1/verify/z3 -d '{
+  "input": {"constraints_smt2": "(declare-const age Int) (assert (>= age 18))"}
+}'
+# => check-sat: sat
+```
+
+Each task's `representations.smt2` is pre-shaped for this endpoint
+(`declarations` + `policy_assertion`); the documented `expected_check_sat` is
+the result for the allow-path formula. Encoding notes (role/region/country
+integer codes, day-of-week numbering) are recorded in each file's `smt2.notes`
+and in the per-task summaries above so the future `internal/symbolic`
+path-explorer can consume them without re-deriving the mapping.
diff --git a/bench/policy-compliance-fixtures/auth-minimum-age.json b/bench/policy-compliance-fixtures/auth-minimum-age.json
new file mode 100644
index 0000000..c0c6907
--- /dev/null
+++ b/bench/policy-compliance-fixtures/auth-minimum-age.json
@@ -0,0 +1,37 @@
+{
+  "id": "auth-minimum-age",
+  "title": "Minimum-age authorization gate",
+  "category": "authorization",
+  "complexity": "simple",
+  "description": "A principal may access a resource only if their declared age is at least the minimum threshold (18). This is the smallest meaningful policy: a single relational condition with two reachable branches (grant / deny). It is the baseline against which the more complex fixtures are compared.",
+  "policy_rules": [
+    "The principal's age MUST be greater than or equal to 18 to be authorized.",
+    "Any age below 18 MUST be denied regardless of other attributes."
+  ],
+  "expected_behavior": "An access request evaluates to allow when age >= 18 and to deny when age < 18. The boundary value age == 18 must be allowed (closed lower bound). Both branches are independently feasible, so a symbolic explorer must enumerate two paths and a concrete tester must observe both verdicts.",
+  "paths": [
+    { "id": "allow", "condition": "age >= 18", "verdict": "allow", "feasible": true, "witness": { "age": 18 } },
+    { "id": "deny", "condition": "age < 18", "verdict": "deny", "feasible": true, "witness": { "age": 12 } }
+  ],
+  "representations": {
+    "cel": {
+      "endpoint": "POST /v1/verify/criterion",
+      "verify_method": "cel_expr",
+      "expr": "age >= 18",
+      "context_template": { "age": 0 }
+    },
+    "smt2": {
+      "endpoint": "POST /v1/verify/z3",
+      "declarations": "(declare-const age Int)",
+      "policy_assertion": "(assert (>= age 18))",
+      "expected_check_sat": "sat",
+      "notes": "Integer age; the policy assertion is the allow-path condition, so check-sat is sat with model age=18."
+    }
+  },
+  "samples": [
+    { "name": "adult", "context": { "age": 25 }, "expected_cel": true, "expected_path": "allow" },
+    { "name": "boundary-min", "context": { "age": 18 }, "expected_cel": true, "expected_path": "allow" },
+    { "name": "one-below-min", "context": { "age": 17 }, "expected_cel": false, "expected_path": "deny" },
+    { "name": "minor", "context": { "age": 12 }, "expected_cel": false, "expected_path": "deny" }
+  ]
+}
diff --git a/bench/policy-compliance-fixtures/data-residency-geo.json b/bench/policy-compliance-fixtures/data-residency-geo.json
new file mode 100644
index 0000000..93dc6e5
--- /dev/null
+++ b/bench/policy-compliance-fixtures/data-residency-geo.json
@@ -0,0 +1,43 @@
+{
+  "id": "data-residency-geo",
+  "title": "Data-residency / geo-fencing compliance (conjunctive predicate set with negated membership)",
+  "category": "data-protection",
+  "complexity": "complex",
+  "description": "A record may be persisted only when ALL of the following hold: it is stored in the EU residency region, it is not in a blocked-country set, and it is encrypted at rest. This fixture exercises a conjunction of heterogeneous predicates (equality on an enumerated region, negated membership over a country blocklist, and a boolean flag), which is the most predicate-dense policy in the set and stresses both path enumeration and the solver's conjunction reasoning.",
+  "policy_rules": [
+    "region MUST equal \"EU\".",
+    "country MUST NOT be a member of the blocked set {\"X\", \"Y\"}.",
+    "encrypted MUST be true.",
+    "The record is allowed only when ALL three rules hold simultaneously."
+  ],
+  "expected_behavior": "The record is allowed only when region == EU AND country is not blocked AND encrypted == true. Each predicate fails independently, so there are three deny sub-paths (wrong region, blocked country, unencrypted) in addition to the single allow path. In the SMT-LIB encoding, region is mapped to an integer code (EU=1) and country to integer codes (blocked: X=10, Y=11).",
+  "paths": [
+    { "id": "allow-compliant", "condition": "region == \"EU\" && !(country in [\"X\", \"Y\"]) && encrypted == true", "verdict": "allow", "feasible": true, "witness": { "region": "EU", "country": "DE", "encrypted": true } },
+    { "id": "deny-wrong-region", "condition": "region != \"EU\" && !(country in [\"X\", \"Y\"]) && encrypted == true", "verdict": "deny", "feasible": true, "witness": { "region": "US", "country": "DE", "encrypted": true } },
+    { "id": "deny-blocked-country", "condition": "region == \"EU\" && country in [\"X\", \"Y\"] && encrypted == true", "verdict": "deny", "feasible": true, "witness": { "region": "EU", "country": "X", "encrypted": true } },
+    { "id": "deny-unencrypted", "condition": "region == \"EU\" && !(country in [\"X\", \"Y\"]) && encrypted == false", "verdict": "deny", "feasible": true, "witness": { "region": "EU", "country": "DE", "encrypted": false } }
+  ],
+  "representations": {
+    "cel": {
+      "endpoint": "POST /v1/verify/criterion",
+      "verify_method": "cel_expr",
+      "expr": "region == \"EU\" && !(country in [\"X\", \"Y\"]) && encrypted == true",
+      "context_template": { "region": "", "country": "", "encrypted": false }
+    },
+    "smt2": {
+      "endpoint": "POST /v1/verify/z3",
+      "declarations": "(declare-const region Int)(declare-const country Int)(declare-const encrypted Bool)",
+      "policy_assertion": "(assert (and (= region 1) (not (= country 10)) (not (= country 11)) encrypted))",
+      "expected_check_sat": "sat",
+      "notes": "Conjunction over equality, two negated equalities, and a boolean; region EU=1, blocked countries X=10/Y=11. Satisfiable (e.g. region=1, country=5, encrypted=true)."
+    }
+  },
+  "samples": [
+    { "name": "eu-de-encrypted", "context": { "region": "EU", "country": "DE", "encrypted": true }, "expected_cel": true, "expected_path": "allow-compliant" },
+    { "name": "eu-fr-encrypted", "context": { "region": "EU", "country": "FR", "encrypted": true }, "expected_cel": true, "expected_path": "allow-compliant" },
+    { "name": "us-de-encrypted", "context": { "region": "US", "country": "DE", "encrypted": true }, "expected_cel": false, "expected_path": "deny-wrong-region" },
+    { "name": "eu-x-encrypted", "context": { "region": "EU", "country": "X", "encrypted": true }, "expected_cel": false, "expected_path": "deny-blocked-country" },
+    { "name": "eu-y-encrypted", "context": { "region": "EU", "country": "Y", "encrypted": true }, "expected_cel": false, "expected_path": "deny-blocked-country" },
+    { "name": "eu-de-plaintext", "context": { "region": "EU", "country": "DE", "encrypted": false }, "expected_cel": false, "expected_path": "deny-unencrypted" }
+  ]
+}
diff --git a/bench/policy-compliance-fixtures/rbac-role-check.json b/bench/policy-compliance-fixtures/rbac-role-check.json
new file mode 100644
index 0000000..87f143d
--- /dev/null
+++ b/bench/policy-compliance-fixtures/rbac-role-check.json
@@ -0,0 +1,38 @@
+{
+  "id": "rbac-role-check",
+  "title": "Role-based access control (disjunctive membership)",
+  "category": "authorization",
+  "complexity": "simple",
+  "description": "A write operation is permitted only when the principal holds one of the privileged roles in the allow-set {admin, editor}. This fixture introduces a disjunction over an enumerated domain, exercising the membership-check path that symbolic execution must split into one branch per allow-set member plus a default deny branch.",
+  "policy_rules": [
+    "The principal's role MUST be a member of the allow-set {admin, editor} to write.",
+    "Any role outside the allow-set MUST be denied write access."
+  ],
+  "expected_behavior": "Write is allowed for role == admin or role == editor and denied for every other role. The allow-set has two members, so the symbolic explorer must enumerate three feasible paths (admin, editor, other). In the SMT-LIB encoding, roles are mapped to integer codes: admin=1, editor=2, all other roles=0.",
+  "paths": [
+    { "id": "allow-admin", "condition": "role == \"admin\"", "verdict": "allow", "feasible": true, "witness": { "role": "admin" } },
+    { "id": "allow-editor", "condition": "role == \"editor\"", "verdict": "allow", "feasible": true, "witness": { "role": "editor" } },
+    { "id": "deny-other", "condition": "role != \"admin\" && role != \"editor\"", "verdict": "deny", "feasible": true, "witness": { "role": "viewer" } }
+  ],
+  "representations": {
+    "cel": {
+      "endpoint": "POST /v1/verify/criterion",
+      "verify_method": "cel_expr",
+      "expr": "role == \"admin\" || role == \"editor\"",
+      "context_template": { "role": "" }
+    },
+    "smt2": {
+      "endpoint": "POST /v1/verify/z3",
+      "declarations": "(declare-const role Int)",
+      "policy_assertion": "(assert (or (= role 1) (= role 2)))",
+      "expected_check_sat": "sat",
+      "notes": "Role codes: admin=1, editor=2. The disjunction is satisfiable (e.g. role=1)."
+    }
+  },
+  "samples": [
+    { "name": "admin", "context": { "role": "admin" }, "expected_cel": true, "expected_path": "allow-admin" },
+    { "name": "editor", "context": { "role": "editor" }, "expected_cel": true, "expected_path": "allow-editor" },
+    { "name": "viewer", "context": { "role": "viewer" }, "expected_cel": false, "expected_path": "deny-other" },
+    { "name": "empty", "context": { "role": "" }, "expected_cel": false, "expected_path": "deny-other" }
+  ]
+}
diff --git a/bench/policy-compliance-fixtures/resource-quota.json b/bench/policy-compliance-fixtures/resource-quota.json
new file mode 100644
index 0000000..d95ebcc
--- /dev/null
+++ b/bench/policy-compliance-fixtures/resource-quota.json
@@ -0,0 +1,37 @@
+{
+  "id": "resource-quota",
+  "title": "Resource quota / capacity-arithmetic gate",
+  "category": "resource-access",
+  "complexity": "moderate",
+  "description": "A provisioning request is accepted only when current usage plus the requested amount stays within the tenant's quota limit. This fixture introduces linear integer arithmetic over three variables, exercising the solver's ability to reason about additive capacity rather than simple equality/membership.",
+  "policy_rules": [
+    "used + requested MUST NOT exceed the tenant quota limit.",
+    "The request MUST be denied when used + requested > limit."
+  ],
+  "expected_behavior": "The request is allowed when (used + requested) <= limit and denied when (used + requested) > limit. The boundary case (used + requested == limit) is allowed. Both branches are feasible: a small request against a fresh tenant is allowed; an over-large request is denied.",
+  "paths": [
+    { "id": "allow-within-quota", "condition": "used + requested <= limit", "verdict": "allow", "feasible": true, "witness": { "used": 30, "requested": 20, "limit": 100 } },
+    { "id": "deny-over-quota", "condition": "used + requested > limit", "verdict": "deny", "feasible": true, "witness": { "used": 90, "requested": 20, "limit": 100 } }
+  ],
+  "representations": {
+    "cel": {
+      "endpoint": "POST /v1/verify/criterion",
+      "verify_method": "cel_expr",
+      "expr": "used + requested <= limit",
+      "context_template": { "used": 0, "requested": 0, "limit": 0 }
+    },
+    "smt2": {
+      "endpoint": "POST /v1/verify/z3",
+      "declarations": "(declare-const used Int)(declare-const requested Int)(declare-const limit Int)",
+      "policy_assertion": "(assert (<= (+ used requested) limit))",
+      "expected_check_sat": "sat",
+      "notes": "Linear arithmetic over non-negative integers; satisfiable (e.g. used=0, requested=0, limit=1)."
+    }
+  },
+  "samples": [
+    { "name": "well-within", "context": { "used": 30, "requested": 20, "limit": 100 }, "expected_cel": true, "expected_path": "allow-within-quota" },
+    { "name": "exactly-at-limit", "context": { "used": 80, "requested": 20, "limit": 100 }, "expected_cel": true, "expected_path": "allow-within-quota" },
+    { "name": "one-over-limit", "context": { "used": 81, "requested": 20, "limit": 100 }, "expected_cel": false, "expected_path": "deny-over-quota" },
+    { "name": "far-over-limit", "context": { "used": 90, "requested": 50, "limit": 100 }, "expected_cel": false, "expected_path": "deny-over-quota" }
+  ]
+}
diff --git a/bench/policy-compliance-fixtures/tiered-rate-limit.json b/bench/policy-compliance-fixtures/tiered-rate-limit.json
new file mode 100644
index 0000000..a698efe
--- /dev/null
+++ b/bench/policy-compliance-fixtures/tiered-rate-limit.json
@@ -0,0 +1,41 @@
+{
+  "id": "tiered-rate-limit",
+  "title": "Tiered rate limit with burst allowance (mixed disjunction + conjunction)",
+  "category": "resource-access",
+  "complexity": "complex",
+  "description": "An API request is admitted when it stays under the base rate limit (100 req/min), OR when the caller is a premium-tier principal staying under an elevated burst limit (200 req/min). This fixture combines a disjunction with a nested conjunction that itself mixes an arithmetic bound with an equality predicate, producing the richest branching structure in the set: three distinct feasible paths and a non-trivial satisfiability query.",
+  "policy_rules": [
+    "A request is allowed when request_count <= 100 (base limit).",
+    "A request is also allowed when request_count <= 200 AND tier == \"premium\" (burst limit).",
+    "All other requests MUST be denied."
+  ],
+  "expected_behavior": "The request is allowed under the base limit for any tier, allowed under the burst limit only for premium tier, and denied once request_count exceeds 200 (or exceeds 100 for non-premium). The premium-under-burst path is reachable only via the conjunction (count in (100, 200] AND tier == premium). In the SMT-LIB encoding, tier is mapped to an integer code: premium=1, all other tiers=0.",
+  "paths": [
+    { "id": "allow-under-base", "condition": "request_count <= 100", "verdict": "allow", "feasible": true, "witness": { "request_count": 50, "tier": "free" } },
+    { "id": "allow-premium-burst", "condition": "request_count <= 200 && tier == \"premium\"", "verdict": "allow", "feasible": true, "witness": { "request_count": 150, "tier": "premium" } },
+    { "id": "deny-over-limit", "condition": "request_count > 200 || (request_count > 100 && tier != \"premium\")", "verdict": "deny", "feasible": true, "witness": { "request_count": 250, "tier": "premium" } }
+  ],
+  "representations": {
+    "cel": {
+      "endpoint": "POST /v1/verify/criterion",
+      "verify_method": "cel_expr",
+      "expr": "request_count <= 100 || (request_count <= 200 && tier == \"premium\")",
+      "context_template": { "request_count": 0, "tier": "" }
+    },
+    "smt2": {
+      "endpoint": "POST /v1/verify/z3",
+      "declarations": "(declare-const request_count Int)(declare-const tier Int)",
+      "policy_assertion": "(assert (or (<= request_count 100) (and (<= request_count 200) (= tier 1))))",
+      "expected_check_sat": "sat",
+      "notes": "Mixed disjunction/conjunction; tier code premium=1. Satisfiable (e.g. request_count=50)."
+    }
+  },
+  "samples": [
+    { "name": "free-under-base", "context": { "request_count": 50, "tier": "free" }, "expected_cel": true, "expected_path": "allow-under-base" },
+    { "name": "premium-under-base", "context": { "request_count": 80, "tier": "premium" }, "expected_cel": true, "expected_path": "allow-under-base" },
+    { "name": "premium-in-burst", "context": { "request_count": 150, "tier": "premium" }, "expected_cel": true, "expected_path": "allow-premium-burst" },
+    { "name": "free-over-base", "context": { "request_count": 150, "tier": "free" }, "expected_cel": false, "expected_path": "deny-over-limit" },
+    { "name": "premium-over-burst", "context": { "request_count": 250, "tier": "premium" }, "expected_cel": false, "expected_path": "deny-over-limit" },
+    { "name": "exactly-base", "context": { "request_count": 100, "tier": "free" }, "expected_cel": true, "expected_path": "allow-under-base" }
+  ]
+}
diff --git a/bench/policy-compliance-fixtures/time-window-access.json b/bench/policy-compliance-fixtures/time-window-access.json
new file mode 100644
index 0000000..aef9238
--- /dev/null
+++ b/bench/policy-compliance-fixtures/time-window-access.json
@@ -0,0 +1,41 @@
+{
+  "id": "time-window-access",
+  "title": "Business-hours maintenance window (nested boolean + arithmetic bounds)",
+  "category": "resource-access",
+  "complexity": "moderate",
+  "description": "A privileged maintenance action is permitted only during business hours (09:00-17:00 UTC, inclusive) on a weekday (Monday-Friday). This fixture introduces nested boolean conjunction over arithmetic range checks, exercising the solver's handling of conjunctive bound constraints and the path explosion that comes from combining two independent ranged predicates.",
+  "policy_rules": [
+    "hour MUST be within the inclusive range [9, 17].",
+    "day MUST be within the inclusive range [1, 5], where 1=Monday ... 5=Friday.",
+    "The action is allowed only when BOTH rules hold simultaneously."
+  ],
+  "expected_behavior": "The action is allowed when 9 <= hour <= 17 AND 1 <= day <= 5, and denied otherwise. Each predicate fails independently, producing three deny sub-paths (off-hours, weekend, both) in addition to the single allow path. day is encoded as an integer 1..7 (1=Monday ... 7=Sunday) in both the CEL context and the SMT model.",
+  "paths": [
+    { "id": "allow-business-hours", "condition": "hour >= 9 && hour <= 17 && day >= 1 && day <= 5", "verdict": "allow", "feasible": true, "witness": { "hour": 12, "day": 3 } },
+    { "id": "deny-off-hours", "condition": "(hour < 9 || hour > 17) && day >= 1 && day <= 5", "verdict": "deny", "feasible": true, "witness": { "hour": 23, "day": 3 } },
+    { "id": "deny-weekend", "condition": "hour >= 9 && hour <= 17 && (day < 1 || day > 5)", "verdict": "deny", "feasible": true, "witness": { "hour": 12, "day": 7 } }
+  ],
+  "representations": {
+    "cel": {
+      "endpoint": "POST /v1/verify/criterion",
+      "verify_method": "cel_expr",
+      "expr": "hour >= 9 && hour <= 17 && day >= 1 && day <= 5",
+      "context_template": { "hour": 0, "day": 1 }
+    },
+    "smt2": {
+      "endpoint": "POST /v1/verify/z3",
+      "declarations": "(declare-const hour Int)(declare-const day Int)",
+      "policy_assertion": "(assert (and (>= hour 9) (<= hour 17) (>= day 1) (<= day 5)))",
+      "expected_check_sat": "sat",
+      "notes": "Conjunction of four bound constraints; satisfiable (e.g. hour=12, day=3)."
+    }
+  },
+  "samples": [
+    { "name": "wed-noon", "context": { "hour": 12, "day": 3 }, "expected_cel": true, "expected_path": "allow-business-hours" },
+    { "name": "mon-open", "context": { "hour": 9, "day": 1 }, "expected_cel": true, "expected_path": "allow-business-hours" },
+    { "name": "fri-close", "context": { "hour": 17, "day": 5 }, "expected_cel": true, "expected_path": "allow-business-hours" },
+    { "name": "late-night", "context": { "hour": 23, "day": 3 }, "expected_cel": false, "expected_path": "deny-off-hours" },
+    { "name": "saturday", "context": { "hour": 12, "day": 6 }, "expected_cel": false, "expected_path": "deny-weekend" },
+    { "name": "sunday-night", "context": { "hour": 2, "day": 7 }, "expected_cel": false, "expected_path": "deny-off-hours" }
+  ]
+}
diff --git a/bench/policy_compliance_fixtures_test.go b/bench/policy_compliance_fixtures_test.go
new file mode 100644
index 0000000..6ba3b6e
--- /dev/null
+++ b/bench/policy_compliance_fixtures_test.go
@@ -0,0 +1,319 @@
+// Package bench also pins the policy-compliance fixture corpus shipped in
+// bench/policy-compliance-fixtures/ (issue #249). The tests here serve two
+// purposes:
+//
+//  1. Structural: every fixture file parses, there are exactly six of them,
+//     each declares a complexity in {simple, moderate, complex}, and each
+//     carries the documentation and dual (CEL + SMT-LIB2) representations the
+//     acceptance criteria require.
+//
+//  2. Runnable: each fixture's CEL expression is executed against every one of
+//     its sample contexts through the real internal/cel evaluator — the
+//     concrete verification engine shared by /v1/verify/cel and
+//     /v1/verify/criterion — and the boolean verdict is asserted to match the
+//     fixture's documented expected_cel. This is the "tasks can be executed by
+//     the concrete testing framework" acceptance criterion, pinned so a broken
+//     expression cannot land silently.
+package bench
+
+import (
+	"context"
+	"encoding/json"
+	"math"
+	"os"
+	"path/filepath"
+	"sort"
+	"strings"
+	"testing"
+
+	"github.com/WasmAgent/symkernel/internal/cel"
+)
+
+// fixturePath returns the absolute path to the policy-compliance-fixtures
+// directory under the repository root.
+func fixturePath(t *testing.T) string {
+	t.Helper()
+	return filepath.Join(repoRoot(t), "bench", "policy-compliance-fixtures")
+}
+
+// fixtureTask is the subset of a fixture file's JSON schema that these tests
+// inspect. Field tags mirror the on-disk shape documented in the fixtures
+// README.
+type fixtureTask struct {
+	ID               string `json:"id"`
+	Title            string `json:"title"`
+	Category         string `json:"category"`
+	Complexity       string `json:"complexity"`
+	Description      string `json:"description"`
+	ExpectedBehavior string `json:"expected_behavior"`
+	PolicyRules      []string `json:"policy_rules"`
+	Paths            []struct {
+		ID        string `json:"id"`
+		Condition string `json:"condition"`
+		Verdict   string `json:"verdict"`
+		Feasible  bool   `json:"feasible"`
+	} `json:"paths"`
+	Representations struct {
+		CEL struct {
+			Endpoint      string         `json:"endpoint"`
+			VerifyMethod  string         `json:"verify_method"`
+			Expr          string         `json:"expr"`
+			ContextTemplate map[string]any `json:"context_template"`
+		} `json:"cel"`
+		SMT2 struct {
+			Endpoint          string `json:"endpoint"`
+			Declarations      string `json:"declarations"`
+			PolicyAssertion   string `json:"policy_assertion"`
+			ExpectedCheckSat  string `json:"expected_check_sat"`
+		} `json:"smt2"`
+	} `json:"representations"`
+	Samples []struct {
+		Name         string         `json:"name"`
+		Context      map[string]any `json:"context"`
+		ExpectedCEL  *bool          `json:"expected_cel"`
+		ExpectedPath string         `json:"expected_path"`
+	} `json:"samples"`
+}
+
+// loadFixtures reads and parses every *.json file in the fixtures directory,
+// returning the tasks keyed by their file stem. It fatals if the directory
+// cannot be read or any file fails to parse.
+func loadFixtures(t *testing.T) map[string]fixtureTask {
+	t.Helper()
+	dir := fixturePath(t)
+	entries, err := os.ReadDir(dir)
+	if err != nil {
+		t.Fatalf("read fixtures dir %s: %v", dir, err)
+	}
+	out := make(map[string]fixtureTask)
+	for _, e := range entries {
+		if e.IsDir() || !strings.HasSuffix(e.Name(), ".json") {
+			continue
+		}
+		raw, err := os.ReadFile(filepath.Join(dir, e.Name()))
+		if err != nil {
+			t.Fatalf("read %s: %v", e.Name(), err)
+		}
+		var task fixtureTask
+		if err := json.Unmarshal(raw, &task); err != nil {
+			t.Fatalf("parse %s: %v", e.Name(), err)
+		}
+		stem := strings.TrimSuffix(e.Name(), ".json")
+		out[stem] = task
+	}
+	return out
+}
+
+// TestFixtures_CorpusShape enforces the directory-level acceptance criteria:
+// the fixtures directory exists, contains exactly six task files, the set
+// matches the six documented task ids, and the complexity range spans
+// simple → complex.
+func TestFixtures_CorpusShape(t *testing.T) {
+	tasks := loadFixtures(t)
+
+	want := map[string]bool{ // expected id → seen?
+		"auth-minimum-age":   false,
+		"rbac-role-check":    false,
+		"resource-quota":     false,
+		"time-window-access": false,
+		"tiered-rate-limit":  false,
+		"data-residency-geo": false,
+	}
+	if len(tasks) != len(want) {
+		t.Errorf("expected exactly %d fixture files, got %d", len(want), len(tasks))
+	}
+
+	complexities := map[string]bool{}
+	for stem, task := range tasks {
+		if _, ok := want[stem]; !ok {
+			t.Errorf("unexpected fixture file %q", stem)
+			continue
+		}
+		want[stem] = true
+		if stem != task.ID {
+			t.Errorf("%s: file stem does not match id %q", stem, task.ID)
+		}
+		complexities[task.Complexity] = true
+	}
+	for id, seen := range want {
+		if !seen {
+			t.Errorf("expected fixture %q is missing from the directory", id)
+		}
+	}
+	// The acceptance criteria require a range of complexity, not a single
+	// band. The corpus deliberately spans all three bands.
+	for _, c := range []string{"simple", "moderate", "complex"} {
+		if !complexities[c] {
+			t.Errorf("corpus is missing the %q complexity band (need simple→complex range)", c)
+		}
+	}
+}
+
+// TestFixtures_DocumentationAndStructure validates the per-task acceptance
+// criteria: documentation fields are populated, each task declares multiple
+// reachable paths (branch coverage), and both the CEL and SMT-LIB2
+// representations are present and well-formed.
+func TestFixtures_DocumentationAndStructure(t *testing.T) {
+	tasks := loadFixtures(t)
+
+	// Stable ordering for readable failures.
+	stems := make([]string, 0, len(tasks))
+	for s := range tasks {
+		stems = append(stems, s)
+	}
+	sort.Strings(stems)
+
+	for _, stem := range stems {
+		task := tasks[stem]
+		t.Run(stem, func(t *testing.T) {
+			if task.Title == "" || task.Description == "" || task.ExpectedBehavior == "" {
+				t.Errorf("missing documentation: title/description/expected_behavior must all be set")
+			}
+			if len(task.PolicyRules) == 0 {
+				t.Errorf("policy_rules must list at least one rule")
+			}
+			switch task.Complexity {
+			case "simple", "moderate", "complex":
+			default:
+				t.Errorf("complexity %q is not one of simple|moderate|complex", task.Complexity)
+			}
+
+			// Path coverage: at least one allow and one deny, all feasible.
+			if len(task.Paths) < 2 {
+				t.Errorf("paths must enumerate at least 2 branches for coverage, got %d", len(task.Paths))
+			}
+			sawAllow, sawDeny := false, false
+			known := map[string]bool{}
+			for _, p := range task.Paths {
+				if p.ID == "" || p.Condition == "" {
+					t.Errorf("path entry missing id/condition: %+v", p)
+				}
+				switch p.Verdict {
+				case "allow":
+					sawAllow = true
+				case "deny":
+					sawDeny = true
+				default:
+					t.Errorf("path %q has verdict %q, want allow|deny", p.ID, p.Verdict)
+				}
+				if !p.Feasible {
+					t.Errorf("path %q must be feasible (witness-reachable) for meaningful coverage", p.ID)
+				}
+				known[p.ID] = true
+			}
+			if !sawAllow || !sawDeny {
+				t.Errorf("paths must include at least one allow AND one deny branch")
+			}
+
+			// CEL representation: non-empty expression addressed to the
+			// criterion endpoint via cel_expr.
+			cel := task.Representations.CEL
+			if cel.Endpoint == "" || cel.VerifyMethod != "cel_expr" || cel.Expr == "" {
+				t.Errorf("representations.cel must set endpoint, verify_method=cel_expr, and a non-empty expr")
+			}
+			if len(cel.ContextTemplate) == 0 {
+				t.Errorf("representations.cel.context_template must declare the input variables")
+			}
+
+			// SMT-LIB2 representation: declarations + a policy assertion that
+			// encodes the allow path, plus the documented check-sat result.
+			smt := task.Representations.SMT2
+			if !strings.Contains(smt.Declarations, "declare-const") {
+				t.Errorf("representations.smt2.declarations must declare at least one constant: %q", smt.Declarations)
+			}
+			if !strings.HasPrefix(strings.TrimSpace(smt.PolicyAssertion), "(assert") {
+				t.Errorf("representations.smt2.policy_assertion must be an (assert ...) form: %q", smt.PolicyAssertion)
+			}
+			if smt.ExpectedCheckSat != "sat" && smt.ExpectedCheckSat != "unsat" {
+				t.Errorf("representations.smt2.expected_check_sat must be sat|unsat, got %q", smt.ExpectedCheckSat)
+			}
+
+			// Samples: golden cases that name an expected verdict and a path
+			// documented above.
+			if len(task.Samples) == 0 {
+				t.Fatalf("samples must contain at least one golden case")
+			}
+			for _, s := range task.Samples {
+				if s.Name == "" {
+					t.Errorf("sample missing name")
+				}
+				if s.ExpectedCEL == nil {
+					t.Errorf("sample %q missing expected_cel", s.Name)
+				}
+				if !known[s.ExpectedPath] {
+					t.Errorf("sample %q references unknown expected_path %q", s.Name, s.ExpectedPath)
+				}
+			}
+		})
+	}
+}
+
+// TestFixtures_ConcreteCEL executes every fixture's CEL expression against
+// every sample context through the real internal/cel evaluator and asserts the
+// boolean verdict matches the documented expected_cel. This proves the corpus
+// is runnable by the concrete testing framework (the CEL engine behind
+// /v1/verify/cel and /v1/verify/criterion).
+func TestFixtures_ConcreteCEL(t *testing.T) {
+	tasks := loadFixtures(t)
+
+	stems := make([]string, 0, len(tasks))
+	for s := range tasks {
+		stems = append(stems, s)
+	}
+	sort.Strings(stems)
+
+	ctx := context.Background()
+	for _, stem := range stems {
+		task := tasks[stem]
+		expr := task.Representations.CEL.Expr
+		if expr == "" {
+			t.Fatalf("%s: missing CEL expr", stem)
+		}
+		t.Run(stem, func(t *testing.T) {
+			for _, s := range task.Samples {
+				if s.ExpectedCEL == nil {
+					t.Fatalf("%s/%s: sample missing expected_cel", stem, s.Name)
+				}
+				t.Run(s.Name, func(t *testing.T) {
+					// JSON decodes every number as float64, but CEL type
+					// inference then maps it to DoubleType and rejects
+					// comparisons against int literals (e.g. age >= 18).
+					// Convert whole numbers back to int64, mirroring the
+					// production /v1/verify/cel handler's normalizeContext.
+					vars := normalizeNumbers(s.Context)
+					got, err := cel.Evaluate(ctx, expr, vars)
+					if err != nil {
+						t.Fatalf("%s/%s: cel.Evaluate: %v", stem, s.Name, err)
+					}
+					ok, ok2 := got.(bool)
+					if !ok2 {
+						t.Fatalf("%s/%s: CEL expr returned %T, want bool", stem, s.Name, got)
+					}
+					if ok != *s.ExpectedCEL {
+						t.Errorf("%s/%s: CEL verdict = %v, want %v (path %q)",
+							stem, s.Name, ok, *s.ExpectedCEL, s.ExpectedPath)
+					}
+				})
+			}
+		})
+	}
+}
+
+// normalizeNumbers returns a copy of m in which whole-number float64 values
+// (the result of encoding/json's default number decoding) are converted to
+// int64 so that CEL infers IntType rather than DoubleType. This mirrors
+// internal/cel.normalizeContext — the same preparation the production
+// /v1/verify/cel handler applies to inbound request contexts.
+func normalizeNumbers(m map[string]any) map[string]any {
+	out := make(map[string]any, len(m))
+	for k, v := range m {
+		if f, ok := v.(float64); ok {
+			if f == math.Trunc(f) && !math.IsInf(f, 0) && !math.IsNaN(f) {
+				out[k] = int64(f)
+				continue
+			}
+		}
+		out[k] = v
+	}
+	return out
+}