Adding limit decrement and checking to BVA
In case there is a bug with assumptions parsing, print info about it
Check for okay() after Solver::solve() and exit fast

This is needed for assumptions check
More debug printing in BVA
Merge branch 'bug_with_bva'