Bounded-like checker for LTS

[kris7t]

This patch adds a bounded-like model checker that can work with LTS. This allows use to use BMC for models that can't be converted to MonolithicExpr directly, or when such conversion introduces a large overhead. Another benefit is testing new features (e.g., XCFA labels) that are only implemented in the LTS and TransFunc level, without having to provide a corresponding MonolithicExpr implementation.

• Adds BoundedLtsChecker, a checker that expands and LTS and an Analysis like an Abstractor, but applies a BMC-like procedure to call an SMT solver after every expanded transition and finally deliver a safe/unsafe/unknown verdict.
• In theory, the bounded-like checker could be used with any Analysis and Prec. Such a configuration would use the specified level of abstraction to enumerate transitions without passing the full path condition to the SMT solver before checking the full path condition like a BMC. However, we currently only use the unit abstraction, meaning that fireability is entirely determined by full path condition checking.
• Adds UnitXcfaAnalysis, anAnalysis that uses the unit abstraction for XCFA. This analysis is not suitable for CEGAR, as it cannot be refined, but it lets BoundedLtsChecker handle the full path condition.