小编Kur*_*tov的帖子

我正在尝试解决数组表达式的模型，其中数组的默认值等于 0。

例如，我试图解决这个例子，但我一直得到未知的结果

(declare-const arr (Array Int Int))
(declare-const arr2 (Array Int Int))
(declare-const a Int)
(declare-const b Int)

(assert (forall ((x Int)) (= (select arr x) 0)))

(assert (> a 0))
(assert (<= a 10))

(assert (= arr2 (store arr a 1337)))

(assert (> b 0))
(assert (<= b 10))


(assert (= (select arr2 b) 0))

(check-sat)
(get-model)