Sketch

linguistic support for sketching

Counterexample-driven solver:

What is control c? Is it concrete? In which step of the algorithm that the program is made finite?
Intuitively, I can’t see why this algorithm is working

Pruning out impossible controls by accumulating all critical, discriminating inputs.