We developed a program synthesis framework for transfer functions on integer abstract domains. First, it utilizes formal semantics of operations described by SMT dialect in MLIR and proves the soundness and precision of synthesized transfer functions. Second, instead of generating a lengthy function, it synthesizes a collection of small transfer functions and combines a set of them to form the final transfer function with the best precision. Finally, we evaluate our work by comparing synthesized transfer functions with those in LLVM, showing that some are more precise. Besides, under our framework, we can show the capability of synthesizing transfer functions for combined operations or equipped with special preconditions. In summary, we believe that, assisted by our framework, programmers can be more confident and braver when exploring optimization opportunities and new domains in data-flow analysis.