New CEGIS with bounded-sized grammar, Bs as global variables

CEGIS works with a fresh program

CEGIS needs to inject chooses of which it updates the implementation,
this is done on a fresh program to avoid these changes to propagate to
other parts of synthesis.

For now we only use DefaultEvaluator with the C-Tree program, since
global variables are not supported in codegen evaluator yet.