当我试图获得一个模型字符串,以及我定义的变量时,我在模型中得到额外的输出 -
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正在使用的一些中间变量？
因为我定义的变量的值对我来说似乎没问题.我之前没有见过任何这样的输出,因此我怀疑了.
Z3有几个预处理步骤.其中一些引入了新的变量.通常会从结果模型中删除新变量.如果他们不是,这是一个错误.然而,这个错误并不会影响正确性.这只是一个不便之处.
如果你能发布你的问题会很棒.我们将能够确定哪个预处理步骤没有消除引入的辅助变量.