java_verify happily uses method overrides with the wrong types

[brianhuffman]

For example: Suppose Java method foo operates on arrays of arbitrary size. We can use java_verify to prove a method override foo_thm for foo with the array size fixed at, say, 10. Then suppose that method bar calls foo with an array argument of size 5. If we run java_verify on bar, passing in foo_thm as an override, then the generated proof obligations will be ill-typed.

In the LWE proofs (e.g. revision 96bc7d74 of saw-examples) this eventually produces errors like the following when we try to run z3 via the SBV backend:

Checking final assertions
./Data/Vector/Generic.hs:400 (slice): invalid slice (90,10,10)

To fix this, java_verify should compare the types of method overrides with the array sizes in the calling context, and refuse to apply the override if the types don't match.