look at a != null

compareSpec (edslSrc, "swap_spec1") (edslSrc, "swap_spec2")

Will output:

pre1:
a != null && a.length > 0 && i >= 0 && j >= 0

pre2:
a != null && a.length > 0 && i >= 0 && j > 0

formulas are NOT equivalent, model:
j -> 0
i -> 0
a.length -> 1
a -> 1

Apparently it is assumed that a is of type int, while it's actually int[]