Handling multiple solvers is still ugly. In particular, one area this shows up is when the original transition system is different than the solver used in the engine. This is currently fairly ugly and inefficient. Additionally, it's easy to forget to set the original TS in some edge cases. For example, #255 included a fix for IC3IA where the original TS was lost. This is because it passes a fresh TS as the "main" one because that is the abstraction that other members needed access to right away (e.g. the abstractor classes) for modifying it. But then the orig_ts_ was not set correctly so we had to manually do that. But there's no infrastructure for ensuring that happens properly.
Handling multiple solvers is still ugly. In particular, one area this shows up is when the original transition system is different than the solver used in the engine. This is currently fairly ugly and inefficient. Additionally, it's easy to forget to set the original TS in some edge cases. For example, #255 included a fix for IC3IA where the original TS was lost. This is because it passes a fresh TS as the "main" one because that is the abstraction that other members needed access to right away (e.g. the abstractor classes) for modifying it. But then the orig_ts_ was not set correctly so we had to manually do that. But there's no infrastructure for ensuring that happens properly.