Tools for formal verification of complex systems often encounter problems of infinite size, making solutions with explicit representations impossible. Even for finite systems, formal verification is often infeasible when expecting an answer in reasonable time due to exponential complexity of the underlying algorithms. This report demonstrates the occurrence of such complexity challenges in our verification tool, which is based on graph transformation systems and inductive invariants. As two orthogonal approaches to such challenges, the report explains symbolic representation for negative application conditions and constraint reasoning. Both techniques have already been seen to significantly reduce the algorithm̢۪s runtime for specific examples.