Repository navigation
Explorer fails on very large traces (RecursionError building the execution tree) #59
Description
When a run hits a StackOverflowError on a symbolic path, the trace contains ~11k branches and the explorer stalls while processing it (minutes of constraint parsing/cache lookups, no new rounds).
Reproducer:
static int rec(int n) {
if (n == 42) return rec(n);
return n;
}
public static void main(String[] args) {
int x = Verifier.nondetInt();
rec(x);
assert x != 7;
}Expected: the explorer handles the large trace in reasonable time (or bounds it) and continues exploring, finding x == 7.
Not caused by the witness changes (#57); same behavior on dev.
Activity
nils-loose commentedon Oct 15, 2026
The full Java run (2026-10-15) found the cause on regular tasks.
data/BinaryExecutionTree/Node.__init__builds the tree with nestedNode(...)constructor calls, one per branch. On Python ≥ 3.12 these recurse through the C stack, sosys.setrecursionlimitdoesn't help and traces of about 3,300 branches raiseRecursionError. The run then hangs (#62).35 runs affected:
Fix: build the tree iteratively.
[-]Explorer stalls on very large traces (e.g. StackOverflowError)[/-][+]Explorer fails on very large traces (RecursionError building the execution tree)[/+]nils-loose commentedon Oct 20, 2026
Fixed in #72, merged into
devthrough #92.