 生成的代码中的存在两个重复的postcondition cheking,一个在判断语句内所以找得到临时变量,一个在外面会报错。 