Interpreter ignores in-path assumptions

[bafain]

The following annotations fail when executed by the interpreter but should succeed.

_assume false
_assert 0 = 1

and

if (true) {
    _assume false
}
_assert 0 = 1

But note that it is still correct that the now following annotations succeed, because the conditional branch is not executed and the assumption therefore is not on one path with the assertion.

if (false) {
    _assume false
}
_assert 0 = 1

This is related to #99 because axioms have not only to be passed for help but also because they change the truth value of the evaluated assertions just like assumptions do.

[bafain]

I think that the interpreter can collect the assumptions, adding them to its internal state, just as they are executed along the way since its execution path is exactly the single path to be asserted by the interpreter instance (compared to all paths asserted by the prover). This implies that the new visitors created for executing functions do not include the main block's assumptions - but still the axioms. Now when an assertion is reached the implication of the assertion by the assumptions, which includes the axioms, is to be evaluated and not only the asserted expression. The tricky point now is that when a QuantifiedExpression is visited during evaluation the whole implication has to be passed to the prover and not only the just visited QuantifiedExpression, which is the reason why #38 is still a fixed bug.

[bafain]

RuntimeAssertionTests (see examples in the issue description above) still fail. This is not solved by "[passing] assumptions/axioms to prover" since the interpreter evaluates some assertions (the not quantified ones) itself, the interpreter also has to evaluate the implication of each assertion by the assumptions.

[bafain]

1. assumptions and axioms are tried to be proven again (reopen #38)

2. the interpreter does not remember that there were false axioms or assumptions but true once:

   _assume false
   _assume true
   // EXPECTED:VALID but ACTUAL:INVALID
   _assert 0 = 1