Segmentation fault: 11

[shazqadeer]

blah.txt

When I run z3 version 4.8.5 on the attached file (apologies I had to rename the file to have a .txt extension to make the upload easy), I get a segmentation fault.

shaz-mbp:Downloads shaz$ z3 -version
Z3 version 4.8.5 - 64 bit
shaz-mbp:Downloads shaz$ pwd
/Users/shaz/Downloads
shaz-mbp:Downloads shaz$ z3 blah.smt2
unsat
Segmentation fault: 11

[shazqadeer]

Here is a smaller repro obtained by deleting stuff from the original file.
blah.txt

[shazqadeer]

blah.txt
Here is the smallest example I could construct. There are only two constraints in the formula and if I comment out any one of them the seg fault does not happen.

[NikolajBjorner]

Thanks, it is related to algebraic datatypes + arrays in a nested setting. Model generation isn't fully fleshed out there so examples are useful to figure out what has to be done. Workaround until this is fixed is to avoid nested recursive types under arrays (such as (Map (|m#Map| (Array T@Edge T@Value)), where T@Value is defined).

[NikolajBjorner]

Fix was checked in on August 10'th. The crash is no longer.