Goal-Directed Invariant Synthesis for Model Checking Modulo Theories