treatment of new in SymbExe

[rgrig]

The type inferer wrongly identifies which objects are initialized by INVOKESPECIAL. It is possible, for example, to execute the same NEW twice before executing a corresponding INVOKESPECIAL.

[rgrig]

It does not work to use an object ID instead of a (NEW) instruction ID. If a NEW instruction is executed twice, then symbolic execution has no choice but to unify the two object IDs, therefore losing any advantage. (Unifying in a set would diverge.)

It also does not work to keep track of all objects that are created and not yet initialized because there might be an unbounded number of those. We certainly don't want to count how many times loops are executed, anyway.

The current implementation is OK, but we must also implement an extra check. Whenever we execute a NEW, there must exist no initialized object that was created by the same NEW.

[rgrig]

Fixed by b0563cb