Concrete random testing

Draw two independent random 64-bit values and check RAX == RBX.

RAX
RBX
Attempts
0
Hits (RAX == RBX)
0

Start auto-run to estimate how long a match would take.

Symbolic solve

RAX = α, RBX = β. Path constraint to reach target: α == β.

RAXα
RBXβ