当我尝试获取一个模型字符串时,除了我定义的变量外,我在模型中会得到额外的输出 -
z3name!0=3, z3name!1=-2, z3name!10=0, z3name!11=0, z3name!12=0, z3name!13=0, z3name!14=0, z3name!15=0, z3name!2=0, z3name!3=0, z3name!4=2, z3name!5=2, z3name!6=0, z3name!7=-3, z3name!8=2, z3name!9=0
我想知道这是否是错误的输出?或者这是Z3正在使用的一些中间变量吗?
因为我定义的变量的值对我来说似乎都是正确的。我以前从未见过这样的输出,因此我产生了疑问。