вот контекст Z3:
(forall ((X (Array Int (Array Int Real))) (i Int) (j Int))
(let ((a!1 (* (- 1) (to_int (select (select X i) j)))))
(= (+ (testArr X i j) a!1) 0))))
это означает:
forall X,i,j. testArr(X,i,j) == X[i][j]
теперь я пытаюсь доказать два похожих утверждения:
1 (=> (= (select (select Z i1) j1) (select (select X i) j))
(= (select (select Z i1) j1) (testArr X i j)))
а также
2 (=> (= v (select (select X i) j))
(= v (to_real (testArr X i j))))
второе утверждение Z3 возвращает действительное значение, но первое утверждение Z3 возвращает неверное значение, а в другом примере Z3 иногда возвращает неизвестное значение. почему??