There is an unsaved comment in progress. You will lose your changes if you continue. Are you sure you want to reopen the work item?
doubt on multidimensional arrays
I am using z3 and I face following problem:
arr is my two dimensional array.
In my code I am assigning bit-vector to one of the row of the array in the following manner.
arr[i]=write_bv (write_bv is bit-vector of size 5 )
I want to store write_bv bit-vector at the 'ith row' of arr.
(declare-fun arr () (Array ( BitVec 3) (Array ( BitVec 3) (_ BitVec 1) )))
(store arr i write_bv)
The above code give error as sort-mismatch.
So how should one write such cases.