转化为合金6

Question

我第一次运行合金6 (6.1.0)。我已经更新了我的语法，并且没有收到错误消息。但是我经常检查断言(在合金5中是有效的)：

0瓦尔斯。0个初级vars。507毫秒。没有发现反例。断言可能有效。0毫秒

这不可能是对的我该怎么办？

Answer 1

答案是通过私人邮件给出的。这个问题并不是针对合金6的，因为这种行为在合金5中已经存在:事实上，即使不调用SAT求解器，合金也能够解决某些断言，因此在0 vars. 0 primary vars. 507 ms. No counterexample found. Assertion may be valid. 0 ms.中出现了该行为。