Implementing abduction over first order theories
You could use an SMT solver inside a counterexample-guided inductive synthesis loop to learn an expression that fits. The paper below does something similar. If you aren't interested in finding the weakest expression, you could save on computational costs by using templates. 


Albarghouthi, Aws, Isil Dillig, and Arie Gurfinkel. "Maximal specification synthesis." ACM SIGPLAN Notices. Vol. 51. No. 1. ACM, 2016.