Non-incremental solving

[ThomasHaas]

I added the option --eager.incremental=true/false (default true) to change the solving approach of the AssumeSolver (I would rename the class to EagerSolver maybe).
With --eager.incremental=false, a second prover instance is used to check for bounds (btw. we could run this check in parallel!). Since we use two queries now, we cannot dump the generated SMT formulas into a single file, so for now the second query is not dumped (we could use two files though).

This PR is mostly for testing and I don't mind not merging it (though it is not much code).
The interesting use case is if we use --encoding.integers=false and --encoding.wmm.idl2sat=false to generate a pure BV encoding which can be solved by SAT solvers. For example, in this case Z3 will only use its SAT solver to solve the query (if non-incremental, otherwise Z3 still uses the SMT solver).

@hernanponcedeleon, maybe you want to play around with this on some complex benchmarks.

TODO: In case we merge, we might have to register AssumeSolver for native code generation.

[hernanponcedeleon]

For documentation: I did an svcomp run (1 min timeout) for profiling incremental vs non-incremental (using both z3 and yices2) and the differences were almost inexistent. While there were some differences on individual benchmarks (mostly variants of fib and triangular), on the accumulated performance both times were pretty much identical.