当我尝试获取模型字符串以及我定义的变量时，我会在模型中获得额外的输出 -
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 有几个预处理步骤。其中一些引入了新的变量。新变量通常会从结果模型中删除。如果不是，则这是一个错误。但是，此错误不影响正确性。这只是一个不便。
如果您能发布您的问题，那就太好了。我们将能够确定哪个预处理步骤没有消除引入的辅助变量。
关于Z3 4.0 模型中的额外输出，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/10983067/