“Concolic execution is too slow” is an impression I keep running into. I have been making the same counterargument for years: collecting symbolic expressions can be cheap enough to save work overall, especially when the alternative is rerunning the program repeatedly to infer the same information.

With some help from coding agents, I finally made time to test this argument. In a small experiment across 15 targets (five one-hour runs per configuration), SymSan+i2s recorded higher fuzzing throughput on 13 targets and higher median line coverage on 8, with 2 ties, compared against AFL++’s CmpLog/RedQueen. Both configurations ran inside AFL++ with ordinary mutations enabled. When those mutations were disabled, SymSan+i2s achieved higher median line coverage on 12 of the 15 targets.

These results offer a concrete reason to reconsider the blanket claim that concolic execution inevitably slows down a hybrid fuzzer. They also establish a useful baseline for future comparisons with SymSan: both the choice of solver and how it integrates with the fuzzer matter.

What do we want to know?

In hybrid fuzzing, we want inputs that flip branches—either to improve overall coverage or to reach a specific target location. When many input values satisfy a branch condition, random mutation works well. When the condition is tight, such as magic == 0xdeadbeef, guessing a satisfying value is much harder. To get past such checks, we need to answer two questions:

  1. Which input bytes affect the target branch?
  2. How should we change those bytes to satisfy its condition?

There are two broad ways to answer the first question:

  • Trace the dependencies. Taint analysis and symbolic/concolic execution track how input bytes affect values as the program runs. Older engines often incurred heavy overhead from interpreting program instructions. Compile-time engines like SymSan substantially reduce this cost by embedding tracing instrumentation directly into the binary and efficiently maintaining symbolic expressions.
  • Infer the dependencies. Mutate input bytes, rerun the program, and observe which values in branch conditions change. Representative systems include WEIZZ, GREYONE, and PATA.

There are also two main ways to answer the second question:

  • Use a general constraint solver. The classic concolic approach sends symbolic branch conditions to an SMT solver to search for satisfying inputs. This is powerful, but solving complex constraints can easily dominate runtime.
  • Use lightweight heuristics. Cornelius Aschermann and his coauthors observed that values used in comparisons often correspond directly to input bytes, or to simple transformations of them. Their RedQueen system exploits this input-to-state (i2s) correspondence to propose replacements efficiently. The approach is now integrated into AFL++, and I implemented a corresponding i2s solver for SymSan.

Crucially, these two dimensions are orthogonal: collecting symbolic expressions does not lock you into using a heavy, general-purpose solver afterward.

What is the cost?

Using lightweight input-to-state solving on both sides lets us compare the two ways of gathering the underlying information: tracing dependencies in a single pass versus inferring relationships across repeated executions. Because the implementations differ, this setup does not hold solving cost strictly constant, but it avoids the apples-to-oranges trap of comparing a lightweight heuristic against a full SMT solver.

Here, I compare SymSan (using its i2s solver) against AFL++’s CmpLog/RedQueen. CmpLog records comparison operands, which RedQueen uses to suggest input replacements. RedQueen’s preparation includes colorization: mutating segments of an input and rerunning the program to maximize entropy in the input bytes without altering the execution path. This helps establish input-to-state correspondences, though the number of extra executions required depends on both the input and the target program. (Implementation.)

SymSan pays upfront for symbolic tracing instead. Our USENIX Security 2022 paper reported a 9.2× geometric-mean slowdown for tracing without solving (Table 5). Several applications fall between 5× and 20×, though the overhead varies substantially and can be much higher on certain targets.

Here is the core trade-off: if one symbolic trace costs roughly ten ordinary executions, and inferring the relevant relationships requires more than ten probing executions, collecting symbolic expressions directly is already cheaper. While solving and validating proposed inputs still take time in both approaches, the experiments below measure the net effect on end-to-end fuzzing performance (without isolating probing executions separately).

Expressions also tell us more

RedQueen is effective, but its heuristics only cover a fixed set of relationships. Because symbolic expressions record how a branch condition is computed from input bytes, SymSan’s i2s solver has richer context for extending those heuristics.

Consider input[0] + 1 == 42. Because the symbolic expression preserves the addition, the solver can invert the operation directly and propose input[0] = 41 without invoking a full SMT solver. Recording the computation itself—rather than only observing its concrete operands—makes it straightforward to reason about transformations and handle cases beyond standard pattern matching.

None of the four configurations below used JIGSAW or Z3. The SymSan runs relied strictly on the i2s solver. Note that the coverage results measure the combined impact of tracing and solving; they do not isolate which specific expression patterns drove each gain.

The experiment

I evaluated four configurations built on AFL++ 4.31c:

Configuration CmpLog/RedQueen SymSan+i2s
With havoc CmpLog/RedQueen (-l 2AT) + ordinary AFL++ mutations SymSan custom mutator (i2s only) + ordinary AFL++ mutations
Without havoc CmpLog/RedQueen (ordinary mutations disabled) SymSan+i2s (ordinary mutations disabled)

For the “without havoc” runs, I set AFL_CUSTOM_MUTATOR_ONLY=1 to disable AFL++’s standard deterministic, havoc, and splice stages, leaving only CmpLog/RedQueen or the SymSan custom mutator active.

Each configuration ran five times for one hour per target, using identical seed inputs and test drivers. Runs were pinned to physical CPU cores with strict limits on concurrency and memory. Final line coverage was measured by replaying the resulting corpus through gcov, ensuring a uniform metric across both methods.

To measure throughput, I used AFL++’s recorded execution count over the fixed one-hour budget (which includes time spent tracing and solving). Because AFL++’s counter does not separately track executions inside the out-of-process symbolic tracer, this metric reflects recorded fuzzer throughput rather than the raw sum of all target executions.

With havoc: performance in a hybrid fuzzer

This test asks whether symbolic tracing paired with i2s solving can keep pace with CmpLog/RedQueen when both run alongside standard AFL++ mutations.

The tables below report median line coverage and median throughput (recorded executions divided by the 3,600-second budget) across the five trials.

Target CmpLog/RedQueen
Coverage (lines)		 SymSan+i2s
Coverage (lines)		 CmpLog/RedQueen
Throughput (exec/s)		 SymSan+i2s
Throughput (exec/s)
libyaml 1,857 1,922 2,735.42 3,000.01
libmatheval 883 881 2,807.94 3,033.89
bc 2,171 2,111 754.19 1,127.03
confetti 614 606 2,585.57 3,310.96
krep 417 417 1,660.67 1,514.58
woff2 2,150 2,187 615.74 751.53
oggenc 342 342 38.59 32.11
libxml2 7,115 7,824 1,355.03 1,961.14
libexpat 2,871 2,906 2,271.21 2,677.42
sqlite 15,742 15,199 1,528.09 1,889.14
unqlite 5,178 5,246 488.46 813.21
mujs 4,886 4,952 1,164.53 1,535.85
quickjs 14,242 14,706 874.83 1,189.55
json-c 1,109 1,102 2,046.02 2,530.41
jansson 1,200 1,209 2,600.74 2,826.62

Throughput: SymSan+i2s led on 13 of 15 targets, with a median per-target speedup of 1.24× (roughly 24% higher recorded throughput). Its largest gain was on unqlite (1.66×), while trailing only on krep and oggenc.

Line coverage: SymSan+i2s came out ahead on 8 targets, tied on 2, and trailed on

  1. Its largest margin was on libxml2 (+709 lines, or ~10%), whereas CmpLog/RedQueen saw its biggest lead on sqlite (+543 lines). Higher throughput helps, though it does not guarantee higher coverage on every target.

Without havoc: a more direct comparison

Disabling ordinary mutations removes a major source of shared coverage growth, making this a more direct comparison of symbolic tracing plus i2s and CmpLog/RedQueen. It still compares the complete methods, including how they select inputs and branches to process.

Target CmpLog/RedQueen
Coverage (lines)		 SymSan+i2s
Coverage (lines)		 CmpLog/RedQueen
Throughput (exec/s)		 SymSan+i2s
Throughput (exec/s)
libyaml 723 1,809 0.35 56.77
libmatheval 504 668 0.04 0.71
bc 1,074 1,701 1.73 56.81
confetti 519 600 4.95 120.54
krep 407 398 0.13 0.01
woff2 1,891 1,813 36.31 1.44
oggenc 316 332 3.22 0.50
libxml2 5,771 6,789 31.53 190.70
libexpat 2,045 1,953 14.88 12.75
sqlite 10,792 12,947 11.83 928.53
unqlite 4,019 5,091 10.56 512.68
mujs 3,176 4,389 8.36 506.81
quickjs 7,878 12,813 15.76 749.84
json-c 864 1,018 4.28 42.09
jansson 972 1,067 1.84 13.33

Line coverage: Without havoc, SymSan+i2s won on 12 of 15 targets, with zero ties. Its largest gain was on quickjs (+4,935 lines, or ~63%), while CmpLog/RedQueen led on krep, woff2, and libexpat.

Recorded executions: SymSan+i2s led on 11 of 15 targets, though the throughput differences are much wider than in the havoc runs. Note that ordinary mutations are disabled, recorded executions depend heavily on how many candidate inputs each solver actually yields; a method that proposes few candidates will naturally log very few executions. Consequently, these figures reflect candidate generation volume combined with analysis overhead, rather than raw solver speed alone.

Even with that caveat, the coverage numbers support the effectiveness of SymSan+i2s as a standalone mechanism: once background mutations are removed, its advantage surfaces across far more targets. At the same time, both methods covered fewer lines overall without havoc than with it—confirming that lightweight solving and random mutation remain highly complementary.

For those interested in digging deeper:

Choosing a fair baseline

These numbers also carry a lesson for benchmarking new hybrid fuzzers—such as evaluation in a recent work ConcoLLMic. Benchmarking SymSan via standalone fgtest paired with z3-solver tests a suboptimal setup from SymSan+i2s integrated into AFL++. fgtest is a tool to run unit/regression tests, not a driver for continuous fuzzing. For hybrid fuzzing, the integrated configuration is the more appropriate baseline.

Takeaways

Five one-hour trials across 15 targets is still a modest experiment. Longer campaigns and more repetitions are needed to see how these trends scale. Furthermore, these metrics track coverage and throughput rather than bug discovery, and they do not isolate the exact wall-clock split between dependency recovery and input evaluation.

Still, the data supports the core hypothesis I set out to test: SymSan+i2s can sustain higher fuzzing throughput than CmpLog/RedQueen while achieving higher median line coverage on the majority of targets. Strip away standard havoc mutations, and that coverage lead expands from 8 targets to 12.

For years, this was a back-of-the-envelope argument I had not made time to test head-to-head. With coding agents helping orchestrate the runs and aggregate the data, I finally have the empirical numbers to back it up. Collecting symbolic information has a cost—but gathering it directly can save more work than it takes.