0

次の SMT 式は、矢印の行で x13 が av5 に置き換えられると、rise4fun サイトで構文チェックに失敗します。

(set-info :status unknown) 
;(set-logic QF_BV) 
(declare-fun in3 () (_ BitVec 16)) 
(assert 
(let ((x8 ((_ zero_extend 16) in3))) 
(let ((x13 (ite (not (= x8 (_ bv00000000 32))) (_ bv00045069 32) (_ bv00000174 32)))) 
(let ((av5 (= x13 (_ bv00045069 32)))) 
(= x13 (_ bv4294967295 32)))))) <--------- 
(assert true) 
(check-sat)

エラーメッセージは

Z3(8, 26): エラー: 無効な関数の適用、位置 2 の引数の並べ替えの不一致

私が何を間違っているのでしょうか？

4

1 に答える 1

0

どのバージョンを使用していますか? バージョン 4.3.x を使用しても、不安定な (進行中の) ブランチを使用しても、この問題を再現できません。どちらの場合も、unsat. 私もrise4fununsatに乗ります。

于 2013-02-14T20:47:47.693 に答える