Concolic Branch Lab

Run one concrete input, inspect the collected path condition, then negate one branch and let a tiny bounded solver find the next witness.

run -> record path condition -> flip one branch -> solve -> replay

What this lab shows

A concrete run gives one real path. The branch cards then show how concolic search changes only one decision at a time, solves the new prefix, and replays to see what the program actually does next.

Try this first

Start with the tutorial seed (0, 0). That run stays on the outer false branch. Then flip branch 1, replay (1, 0), and finally flip branch 2 to reach the witness (1, 2).

Start here Set an input, run it concretely, then use one flip card to ask for the next witness in the bounded domain.

Toy program

def f(x, y):
    if x > 0:
        if y == x + 1:
            bug()
    return 0

Current run

Collected path condition

No run yet.

Available branch flips

Detailed log

Explored concrete inputs