[Analysis] Parallel run of Bounded and Unbounded Model checking
Bounded and unbounded model checking have different advantages which can be hardly predictible (sometimes one is faster, sometimes the other is — typically finding a counter example is faster with bounded model checking but proving something valid is faster with normal model checking).
Instead of fixing in the code which one to use, it would be better to run both in parallel and take the result of the first which finishes.
(from redmine: issue id 2277, created on 2015-02-03, closed on 2015-07-29)