Fix functional tests

The variables of type External<T> and Internal<T> which are used
by the program under scrutiny must always be declared inside the
"do { ... } while (find_next_path())" loop.
Avoid unwinding bounds

By default, we always choose the "false" branch. This avoids
getting stuck in infinite loops --- of course, we can only
hope for a semi-decision procedure by the Halting Problem.