z3 - 我如何在 Z3 中用编程语言描述整数除法？

Question

我正在使用 SMT 求解器来帮助分析程序。在编程语言中，可以满足以下条件：

int x;
if((x/2) * 2 != x)  {
//reachable
}

但是对于数学中的整数类型，这是不能满足的。我可以用Z3来形容吗？谢谢。

Answer 1

您的示例在数学整数中也可以满足。您可以找到x任何奇数的模型。

在 Z3 中，您应该使用机器整数，即位向量进行建模：

(declare-const x (_ BitVec 32))
(assert (not (= (bvmul (bvsdiv x (_ bv2 32)) (_ bv2 32)) x)))
(check-sat)
(get-model)

这个示例^{rise4fun 链接}确实可以满足。