z3 - Z3 のプログラミング言語 this で整数除算をどのように記述すればよいですか?

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リンク}の例は、確かに満足のいくものです。