Related Problem
After each state variable insertion, the algorithm must re-elaborate the entire state from scratch. This consumes a lot of time for larger circuits.
Preferred Solution
Annotate the elaborated states with variables that would allow the tool to filter encodings based upon conditional branch of origin. Then, use this to update the state space in linear time with the number of places rather than exponential time.