A few things about array broke

[dzufferey]

It seems that a few examples with arrays broke.

Something seems wrong with the array footprints:

./grasshopper.native -v tests/spl/link_and_array/hashset_no_content_ownership.spl
GRASShopper version 0.5 pre
Selected SMT solvers: Z3
Encoding arrays.
Adding checks for run-time errors.
Eliminating new/free.
Inferring accesses.
Pruning uncalled procedures and predicates.
Eliminating loops.
Eliminating dependencies on global state.
Eliminating SL specifications.
Eliminating unused formal parameters.
Adding frame axioms.
Error: find_proc: Could not find predicate footprint_of_lseg_Array

This example get to this error with and without the simplearrays option. One of the example on which I'm working got to that error without simplearrays and did not throw that exception with simplearrays.

There also seems to be some (re)naming issue:

./grasshopper.native -v tests/spl/array/quicksort.spl 
GRASShopper version 0.5 pre
Selected SMT solvers: Z3
File ".../grasshopper/tests/spl/array/quicksort.spl", line 36, columns 31-32:
Error: Unknown identifier a^1.

[wies]

I fixed the immediate issues with those examples. Do you know what the status of those examples was? Were they supposed to work? The quicksort example currently fails. The other example seems to diverge in Grasshopper. This could be a trigger loop in the provided axioms. The new E-matching engine also generates terms modulo E-matching, which may reveal trigger loops that were masked in the old E-matching engine. I didn't have time yet to investigate what is specifically going on in that example.

[dzufferey]

I'm not sure. I think they were working at some point since they not in the work_in_progress/array folder. But this is just a guess.

When I tried setting up definitions for an unrolled list I encountered this bug. Then I tried the existing examples and found that it also showed up there.