diff --git a/bench/symbolic/bounded_loop_test.go b/bench/symbolic/bounded_loop_test.go
new file mode 100644
index 0000000..30206ff
--- /dev/null
+++ b/bench/symbolic/bounded_loop_test.go
@@ -0,0 +1,11 @@
+package symbolic
+
+import "testing"
+
+func TestBoundedLoopFixture(t *testing.T) {
+	result := runNamedFixture(t, "bounded-loop")
+	assertFixtureResult(t, result, 4)
+	if result.ExploredPaths != 2 {
+		t.Errorf("bounded-loop: explored paths = %d, want 2", result.ExploredPaths)
+	}
+}
diff --git a/bench/symbolic/data_dependent_branches_test.go b/bench/symbolic/data_dependent_branches_test.go
new file mode 100644
index 0000000..8d758dd
--- /dev/null
+++ b/bench/symbolic/data_dependent_branches_test.go
@@ -0,0 +1,11 @@
+package symbolic
+
+import "testing"
+
+func TestDataDependentBranchesFixture(t *testing.T) {
+	result := runNamedFixture(t, "data-dependent-branches")
+	assertFixtureResult(t, result, 4)
+	if result.ExploredPaths != 4 {
+		t.Errorf("data-dependent-branches: explored paths = %d, want 4", result.ExploredPaths)
+	}
+}
diff --git a/bench/symbolic/recursion_test.go b/bench/symbolic/recursion_test.go
new file mode 100644
index 0000000..a29d689
--- /dev/null
+++ b/bench/symbolic/recursion_test.go
@@ -0,0 +1,11 @@
+package symbolic
+
+import "testing"
+
+func TestRecursionFixture(t *testing.T) {
+	result := runNamedFixture(t, "recursion")
+	assertFixtureResult(t, result, 8)
+	if result.ExploredPaths != 3 {
+		t.Errorf("recursion: explored paths = %d, want 3", result.ExploredPaths)
+	}
+}
diff --git a/bench/symbolic/symbolic.go b/bench/symbolic/symbolic.go
new file mode 100644
index 0000000..ad10ec8
--- /dev/null
+++ b/bench/symbolic/symbolic.go
@@ -0,0 +1,206 @@
+// Package symbolic runs the curated WebAssembly symbolic-execution benchmark
+// corpus. It validates concrete execution with wazero and times the matching
+// Z3 path-feasibility queries, including the solver decision-cache hit ratio.
+package symbolic
+
+import (
+	"context"
+	"encoding/base64"
+	"encoding/json"
+	"fmt"
+	"math"
+	"os"
+	"path/filepath"
+	"strings"
+	"time"
+
+	"github.com/WasmAgent/symkernel/internal/z3"
+	"github.com/tetratelabs/wazero"
+)
+
+const manifestName = "manifest.json"
+
+// FixtureRoot is the repository-relative location of the curated corpus.
+const FixtureRoot = "wasmagent/symbolic-fixtures"
+
+// Result is one row in the symbolic benchmark report.
+type Result struct {
+	Fixture           string
+	ExploredPaths     int
+	PotentialPaths    int
+	PathExplosionRate float64
+	SolverTime        time.Duration
+	CacheHitRatio     float64
+}
+
+type manifest struct {
+	Fixtures []fixture `json:"fixtures"`
+}
+
+type fixture struct {
+	Name         string      `json:"name"`
+	Module       string      `json:"module"`
+	Entry        string      `json:"entry"`
+	Arguments    []uint64    `json:"arguments"`
+	BranchPoints int         `json:"branch_points"`
+	Paths        []pathQuery `json:"paths"`
+}
+
+type pathQuery struct {
+	Constraints string         `json:"constraints"`
+	Model       map[string]any `json:"model"`
+}
+
+// Run executes every fixture in root and measures its declared SMT path
+// conditions. Every condition is solved twice: the first pass measures solver
+// work, and the second pass records the decision-cache behaviour.
+func Run(ctx context.Context, root string) ([]Result, error) {
+	corpus, err := loadManifest(root)
+	if err != nil {
+		return nil, err
+	}
+
+	results := make([]Result, 0, len(corpus.Fixtures))
+	for _, f := range corpus.Fixtures {
+		result, err := runFixture(ctx, root, f)
+		if err != nil {
+			return nil, fmt.Errorf("symbolic benchmark %q: %w", f.Name, err)
+		}
+		results = append(results, result)
+	}
+	return results, nil
+}
+
+func loadManifest(root string) (manifest, error) {
+	var corpus manifest
+	data, err := os.ReadFile(filepath.Join(root, manifestName))
+	if err != nil {
+		return corpus, fmt.Errorf("read manifest: %w", err)
+	}
+	if err := json.Unmarshal(data, &corpus); err != nil {
+		return corpus, fmt.Errorf("decode manifest: %w", err)
+	}
+	if len(corpus.Fixtures) == 0 {
+		return corpus, fmt.Errorf("manifest has no fixtures")
+	}
+	return corpus, nil
+}
+
+func runFixture(ctx context.Context, root string, f fixture) (Result, error) {
+	if f.Name == "" || f.Module == "" || f.Entry == "" || len(f.Paths) == 0 {
+		return Result{}, fmt.Errorf("incomplete fixture definition")
+	}
+	if f.BranchPoints < 0 || f.BranchPoints >= 63 {
+		return Result{}, fmt.Errorf("branch_points must be between 0 and 62")
+	}
+	if err := executeModule(ctx, filepath.Join(root, f.Module), f.Entry, f.Arguments); err != nil {
+		return Result{}, err
+	}
+
+	cacheBefore := z3.CacheStats()
+	start := time.Now()
+	feasible, err := solvePaths(ctx, f.Paths)
+	if err != nil {
+		return Result{}, err
+	}
+	solverTime := time.Since(start)
+	if _, err := solvePaths(ctx, f.Paths); err != nil {
+		return Result{}, err
+	}
+	cacheAfter := z3.CacheStats()
+
+	potentialPaths := 1 << f.BranchPoints
+	accesses := cacheAfter.Hits - cacheBefore.Hits + cacheAfter.Misses - cacheBefore.Misses
+	cacheHits := cacheAfter.Hits - cacheBefore.Hits
+	cacheHitRatio := 0.0
+	if accesses > 0 {
+		cacheHitRatio = float64(cacheHits) / float64(accesses)
+	}
+
+	return Result{
+		Fixture:           f.Name,
+		ExploredPaths:     feasible,
+		PotentialPaths:    potentialPaths,
+		PathExplosionRate: float64(feasible) / float64(potentialPaths),
+		SolverTime:        solverTime,
+		CacheHitRatio:     cacheHitRatio,
+	}, nil
+}
+
+func executeModule(ctx context.Context, modulePath, entry string, arguments []uint64) error {
+	encoded, err := os.ReadFile(modulePath)
+	if err != nil {
+		return fmt.Errorf("read module: %w", err)
+	}
+	wasm, err := base64.StdEncoding.DecodeString(strings.TrimSpace(string(encoded)))
+	if err != nil {
+		return fmt.Errorf("decode module: %w", err)
+	}
+
+	runtime := wazero.NewRuntime(ctx)
+	defer runtime.Close(ctx) //nolint:errcheck // context controls runtime teardown
+	module, err := runtime.Instantiate(ctx, wasm)
+	if err != nil {
+		return fmt.Errorf("instantiate module: %w", err)
+	}
+	defer module.Close(ctx) //nolint:errcheck // runtime close releases module resources
+	fn := module.ExportedFunction(entry)
+	if fn == nil {
+		return fmt.Errorf("export %q not found", entry)
+	}
+	if _, err := fn.Call(ctx, arguments...); err != nil {
+		return fmt.Errorf("call %q: %w", entry, err)
+	}
+	return nil
+}
+
+func solvePaths(ctx context.Context, paths []pathQuery) (int, error) {
+	feasible := 0
+	for _, path := range paths {
+		solution, err := z3.SolveConstraintsCtx(ctx, path.Constraints, path.Model)
+		if err != nil {
+			return 0, err
+		}
+		if solution.Sat == "sat" {
+			feasible++
+		}
+	}
+	return feasible, nil
+}
+
+// FormatTable renders benchmark results as a Markdown table suitable for CI
+// logs and benchmark reports.
+func FormatTable(results []Result) string {
+	var b strings.Builder
+	b.WriteString("| Fixture | Paths explored | Potential paths | Path explosion rate | Solver time | Cache hit ratio |\n")
+	b.WriteString("| --- | ---: | ---: | ---: | ---: | ---: |\n")
+	for _, result := range results {
+		fmt.Fprintf(&b, "| %s | %d | %d | %.2f%% | %s | %.2f%% |\n",
+			result.Fixture,
+			result.ExploredPaths,
+			result.PotentialPaths,
+			result.PathExplosionRate*100,
+			result.SolverTime.Round(time.Microsecond),
+			result.CacheHitRatio*100,
+		)
+	}
+	return b.String()
+}
+
+// ValidateResult verifies invariants that callers can use when turning the
+// report into a regression gate.
+func ValidateResult(result Result) error {
+	if result.Fixture == "" || result.PotentialPaths < 1 {
+		return fmt.Errorf("invalid benchmark result")
+	}
+	if result.ExploredPaths < 0 || result.ExploredPaths > result.PotentialPaths {
+		return fmt.Errorf("explored paths outside potential-path range")
+	}
+	if math.IsNaN(result.PathExplosionRate) || result.PathExplosionRate < 0 || result.PathExplosionRate > 1 {
+		return fmt.Errorf("invalid path explosion rate")
+	}
+	if math.IsNaN(result.CacheHitRatio) || result.CacheHitRatio < 0 || result.CacheHitRatio > 1 {
+		return fmt.Errorf("invalid cache hit ratio")
+	}
+	return nil
+}
diff --git a/bench/symbolic/symbolic_test.go b/bench/symbolic/symbolic_test.go
new file mode 100644
index 0000000..b5cc24d
--- /dev/null
+++ b/bench/symbolic/symbolic_test.go
@@ -0,0 +1,130 @@
+package symbolic
+
+import (
+	"context"
+	"encoding/base64"
+	"encoding/json"
+	"os"
+	"os/exec"
+	"path/filepath"
+	"strings"
+	"testing"
+)
+
+func TestSymbolicFixtureCorpus(t *testing.T) {
+	root := filepath.Join("..", "..", FixtureRoot)
+	corpus, err := loadManifest(root)
+	if err != nil {
+		t.Fatalf("loadManifest: %v", err)
+	}
+	if len(corpus.Fixtures) != 3 {
+		t.Fatalf("fixture count = %d, want 3", len(corpus.Fixtures))
+	}
+
+	seen := make(map[string]bool, len(corpus.Fixtures))
+	for _, fixture := range corpus.Fixtures {
+		if seen[fixture.Name] {
+			t.Errorf("duplicate fixture %q", fixture.Name)
+		}
+		seen[fixture.Name] = true
+		if fixture.BranchPoints <= 0 || len(fixture.Paths) == 0 {
+			t.Errorf("%s: missing branch/path declarations", fixture.Name)
+		}
+
+		encoded, err := os.ReadFile(filepath.Join(root, fixture.Module))
+		if err != nil {
+			t.Errorf("%s: read module: %v", fixture.Name, err)
+			continue
+		}
+		if _, err := base64.StdEncoding.DecodeString(strings.TrimSpace(string(encoded))); err != nil {
+			t.Errorf("%s: invalid base64 module: %v", fixture.Name, err)
+		}
+	}
+
+	manifestData, err := os.ReadFile(filepath.Join(root, manifestName))
+	if err != nil {
+		t.Fatalf("read manifest: %v", err)
+	}
+	var decoded map[string]any
+	if err := json.Unmarshal(manifestData, &decoded); err != nil {
+		t.Fatalf("manifest is not JSON: %v", err)
+	}
+}
+
+func runNamedFixture(t *testing.T, name string) Result {
+	t.Helper()
+	if _, err := exec.LookPath("z3"); err != nil {
+		t.Skip("z3 not on PATH")
+	}
+
+	root := filepath.Join("..", "..", FixtureRoot)
+	corpus, err := loadManifest(root)
+	if err != nil {
+		t.Fatalf("loadManifest: %v", err)
+	}
+	for _, fixture := range corpus.Fixtures {
+		if fixture.Name != name {
+			continue
+		}
+		result, err := runFixture(context.Background(), root, fixture)
+		if err != nil {
+			t.Fatalf("runFixture: %v", err)
+		}
+		return result
+	}
+	t.Fatalf("fixture %q not found", name)
+	return Result{}
+}
+
+func assertFixtureResult(t *testing.T, result Result, wantPotentialPaths int) {
+	t.Helper()
+	if err := ValidateResult(result); err != nil {
+		t.Fatalf("%s: %v", result.Fixture, err)
+	}
+	if result.ExploredPaths == 0 {
+		t.Fatalf("%s: explored no feasible paths", result.Fixture)
+	}
+	if result.PotentialPaths != wantPotentialPaths {
+		t.Errorf("%s: potential paths = %d, want %d", result.Fixture, result.PotentialPaths, wantPotentialPaths)
+	}
+	if result.SolverTime <= 0 {
+		t.Errorf("%s: solver time = %s, want positive duration", result.Fixture, result.SolverTime)
+	}
+	if result.CacheHitRatio <= 0 {
+		t.Errorf("%s: cache hit ratio = %f, want a warm-cache hit", result.Fixture, result.CacheHitRatio)
+	}
+}
+
+func TestFormatTable(t *testing.T) {
+	table := FormatTable([]Result{{
+		Fixture:           "bounded-loop",
+		ExploredPaths:     2,
+		PotentialPaths:    4,
+		PathExplosionRate: 0.5,
+		CacheHitRatio:     0.5,
+	}})
+	for _, column := range []string{"Fixture", "Path explosion rate", "Solver time", "Cache hit ratio", "bounded-loop"} {
+		if !strings.Contains(table, column) {
+			t.Errorf("table missing %q:\n%s", column, table)
+		}
+	}
+}
+
+func BenchmarkCuratedFixtures(b *testing.B) {
+	if _, err := exec.LookPath("z3"); err != nil {
+		b.Skip("z3 not on PATH")
+	}
+
+	root := filepath.Join("..", "..", FixtureRoot)
+	var results []Result
+	b.ResetTimer()
+	for range b.N {
+		var err error
+		results, err = Run(context.Background(), root)
+		if err != nil {
+			b.Fatalf("Run: %v", err)
+		}
+	}
+	b.StopTimer()
+	b.Logf("\n%s", FormatTable(results))
+}
diff --git a/internal/z3/z3.go b/internal/z3/z3.go
index 941f0a1..d9036bb 100644
--- a/internal/z3/z3.go
+++ b/internal/z3/z3.go
@@ -25,13 +25,21 @@ type Solution struct {
 	// UnsatCore holds named assertion labels forming the minimal unsat core
 	// when Sat is "unsat" and the input used named assertions.
 	UnsatCore []string `json:"unsat_core,omitempty"`
-	// SolverMs is the elapsed wall-clock time in the Z3 subprocess, in
-	// milliseconds.
+	// SolverMs is the elapsed wall-clock time handling the query, in
+	// milliseconds. Cache hits report cache-lookup time; cache misses report
+	// the Z3 subprocess time.
 	SolverMs int64 `json:"solver_ms"`
 }
 
 var decisionCache = cache.NewFromEnv()
 
+// CacheStats reports aggregate activity for the solver decision cache. It is
+// exposed so benchmark suites can report cache hit ratios without reaching
+// into the cache implementation.
+func CacheStats() cache.Stats {
+	return decisionCache.Stats()
+}
+
 // SolveConstraints submits an SMTLIB2 constraint string to Z3 and returns the
 // result. model is an optional map of variable name → sort hint (or concrete
 // Go value) used to emit (declare-const) declarations before the constraints.
@@ -58,11 +66,11 @@ func SolveConstraintsCtx(ctx context.Context, constraints string, model map[stri
 	if err := ctx.Err(); err != nil {
 		return Solution{Sat: "unknown"}, nil
 	}
+	start := time.Now()
 	if decision, ok := decisionCache.Get(smt2); ok {
-		return solutionFromDecision(decision), nil
+		return solutionFromDecision(decision, time.Since(start)), nil
 	}
 
-	start := time.Now()
 	cmd := exec.CommandContext(ctx, "z3", "-in")
 	cmd.Stdin = strings.NewReader(smt2)
 
@@ -114,12 +122,25 @@ func decisionFromSolution(solution Solution) cache.Decision {
 	}
 }
 
-func solutionFromDecision(decision cache.Decision) Solution {
+func solutionFromDecision(decision cache.Decision, elapsed time.Duration) Solution {
 	return Solution{
 		Sat:       decision.Sat,
 		Model:     decision.Model,
 		UnsatCore: decision.UnsatCore,
+		SolverMs:  elapsedMillis(elapsed),
+	}
+}
+
+// elapsedMillis rounds a completed query up to one millisecond so callers do
+// not mistake a fast cache hit for missing timing metadata.
+func elapsedMillis(elapsed time.Duration) int64 {
+	if elapsed <= 0 {
+		return 0
+	}
+	if millis := elapsed.Milliseconds(); millis > 0 {
+		return millis
 	}
+	return 1
 }
 
 // hasNamedAssertions reports whether the constraints string uses SMTLIB2
diff --git a/internal/z3/z3_test.go b/internal/z3/z3_test.go
index 6270797..19422e5 100644
--- a/internal/z3/z3_test.go
+++ b/internal/z3/z3_test.go
@@ -197,6 +197,28 @@ func TestSolveConstraints_SatIntegration(t *testing.T) {
 	}
 }
 
+func TestSolveConstraints_CacheHitReportsTimingIntegration(t *testing.T) {
+	if _, err := exec.LookPath("z3"); err != nil {
+		t.Skip("z3 not on PATH")
+	}
+
+	constraints := "(assert (> cache_timing_unique 5))"
+	model := map[string]any{"cache_timing_unique": "Int"}
+	if _, err := SolveConstraints(constraints, model); err != nil {
+		t.Fatalf("warm cache: %v", err)
+	}
+	got, err := SolveConstraints(constraints, model)
+	if err != nil {
+		t.Fatalf("cache hit: %v", err)
+	}
+	if got.Sat != "sat" {
+		t.Errorf("Sat = %q, want sat", got.Sat)
+	}
+	if got.SolverMs <= 0 {
+		t.Errorf("SolverMs = %d on cache hit, want positive elapsed timing", got.SolverMs)
+	}
+}
+
 func TestSolveConstraints_UnsatIntegration(t *testing.T) {
 	if _, err := exec.LookPath("z3"); err != nil {
 		t.Skip("z3 not on PATH")
diff --git a/wasmagent/symbolic-fixtures/README.md b/wasmagent/symbolic-fixtures/README.md
new file mode 100644
index 0000000..c997838
--- /dev/null
+++ b/wasmagent/symbolic-fixtures/README.md
@@ -0,0 +1,16 @@
+# Symbolic benchmark fixtures
+
+Each `*.wasm.b64` file is a base64-encoded WebAssembly binary exporting
+`run`. The manifest supplies concrete arguments used to validate that wazero
+can execute the module and SMT-LIB path conditions used by the symbolic
+benchmark.
+
+The corpus intentionally covers the three control-flow patterns most likely
+to cause path growth:
+
+- `bounded-loop`: a decrementing loop with a bounded iteration count.
+- `recursion`: a terminating recursive function with a base case.
+- `data-dependent-branches`: nested branches controlled by two inputs.
+
+Run `go test -v ./bench/symbolic` for the rendered result table and
+`go test -bench . ./bench/symbolic` for repeated measurements.
diff --git a/wasmagent/symbolic-fixtures/bounded-loop.wasm.b64 b/wasmagent/symbolic-fixtures/bounded-loop.wasm.b64
new file mode 100644
index 0000000..c6a6877
--- /dev/null
+++ b/wasmagent/symbolic-fixtures/bounded-loop.wasm.b64
@@ -0,0 +1 @@
+AGFzbQEAAAABBQFgAAF/AwIBAAcHAQNydW4AAAoOAQwAAkADQAwBCwtBAAs=
diff --git a/wasmagent/symbolic-fixtures/data-dependent-branches.wasm.b64 b/wasmagent/symbolic-fixtures/data-dependent-branches.wasm.b64
new file mode 100644
index 0000000..79b800b
--- /dev/null
+++ b/wasmagent/symbolic-fixtures/data-dependent-branches.wasm.b64
@@ -0,0 +1 @@
+AGFzbQEAAAABBwFgAn9/AX8DAgEABwcBA3J1bgAACh4BHAAgAAR/IAEEf0EDBUECCwUgAQR/QQEFQQALCws=
diff --git a/wasmagent/symbolic-fixtures/manifest.json b/wasmagent/symbolic-fixtures/manifest.json
new file mode 100644
index 0000000..9120d9a
--- /dev/null
+++ b/wasmagent/symbolic-fixtures/manifest.json
@@ -0,0 +1,40 @@
+{
+  "fixtures": [
+    {
+      "name": "bounded-loop",
+      "module": "bounded-loop.wasm.b64",
+      "entry": "run",
+      "arguments": [],
+      "branch_points": 2,
+      "paths": [
+        {"constraints": "(assert (= input 0))", "model": {"input": "Int"}},
+        {"constraints": "(assert (and (> input 0) (<= input 4)))", "model": {"input": "Int"}}
+      ]
+    },
+    {
+      "name": "recursion",
+      "module": "recursion.wasm.b64",
+      "entry": "run",
+      "arguments": [3],
+      "branch_points": 3,
+      "paths": [
+        {"constraints": "(assert (= depth 0))", "model": {"depth": "Int"}},
+        {"constraints": "(assert (= depth 1))", "model": {"depth": "Int"}},
+        {"constraints": "(assert (and (> depth 1) (<= depth 3)))", "model": {"depth": "Int"}}
+      ]
+    },
+    {
+      "name": "data-dependent-branches",
+      "module": "data-dependent-branches.wasm.b64",
+      "entry": "run",
+      "arguments": [1, 0],
+      "branch_points": 2,
+      "paths": [
+        {"constraints": "(assert (and (= left 0) (= right 0)))", "model": {"left": "Int", "right": "Int"}},
+        {"constraints": "(assert (and (= left 0) (> right 0)))", "model": {"left": "Int", "right": "Int"}},
+        {"constraints": "(assert (and (> left 0) (= right 0)))", "model": {"left": "Int", "right": "Int"}},
+        {"constraints": "(assert (and (> left 0) (> right 0)))", "model": {"left": "Int", "right": "Int"}}
+      ]
+    }
+  ]
+}
diff --git a/wasmagent/symbolic-fixtures/recursion.wasm.b64 b/wasmagent/symbolic-fixtures/recursion.wasm.b64
new file mode 100644
index 0000000..9f0588b
--- /dev/null
+++ b/wasmagent/symbolic-fixtures/recursion.wasm.b64
@@ -0,0 +1 @@
+AGFzbQEAAAABBgFgAX8BfwMCAQAHBwEDcnVuAAAKFwEVACAARQR/QQAFIABBAWsQAEEBagsL