This paper infer quantifier-free invariant with pre-defined template from program with linear arithmetic and uninterpretated function.
It first translate the problem to linear programing problem by purification, that is, remove the uninterpretated functrion by defining new variable.
And then it solve the problem with linear programing.
博文
