Filter non-det program whenever the tests exclude most paths

In case of timeout when searching for a counter-example, CEGIS will
consider the tentative solution as valid but untrusted. This untrusted
solution will then be validated within the complete solution.