Invariant Synthesis for Incomplete Verification Engines