This project is read-only.


Z3 crashes for the file attached


It actually says segmentation fault.

file attachments

Closed Dec 26, 2012 at 4:42 PM by leodemoura
Problem has been fixed. The fix is already available in the "unstable" (work-in-progress) branch.


leodemoura wrote Dec 26, 2012 at 4:41 PM

Z3 crashed because the input is sort/type incorrect. The problem is the following expression:

((as const(Array ( BitVec 6)( BitVec 1)))write_data_35_0)

write_data_35_0 is a Bit-vector of size 36 instead of a Bit-vector of size 1 as expected by this const operator. I fixed the problem
Now, Z3 returns the error message

(error "line 37 column 106: invalid const array definition, sort mismatch between array range and argument")

for the issuefile.