ето контекста на 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 понякога връща неизвестно. защо??