Hst hst

Fixed superset proof for integer sets

The is_superset_with_proof method would return incorrect proof in

certain situations. When testing A >= B, it's supposed to return an

element of B that's not in A. Since our method works on sorted sets,

it will return the least such element, though this is not a required

part of the method's contract. When A contained an element that was

greater than the least element of B not in A, our method would return

the A element, not the B element. This would cause downstream errors

in the refinement code, in that the wrong counterexample could be

returned in certain situations.

Lighthouse: [#9 state:resolved]

http://github.com/dcreager/hst/c...