Z3 crashes for the file attached


It actually says segmentation fault.

file attachments

Closed Dec 26, 2012 at 3: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 3: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 http://z3.codeplex.com/SourceControl/changeset/2a286541e002.
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.