SMG: fix object inequality checks and value merge/replacement

Refactor objects comparison and value merge/replacement.

AssumeVisitor and SMGState: Unite checks 'an object cannot be the Null object' and general 'an object cannot be (overlap) another object' into private SMGState#areNotEqualObjects. Refactor #comparisonAgainstExternalMemory in #isNotNull and use it in the #areNotEqualObjects. Also use SMGKnownSymbolicValue where possible.

Assume external allocations are different if any has a HVE. If neither has any HVE, they both can be Null, i.e. they are either different, or both Null.

SMG#replaceValue(): Do not replace 0 (do not drop 0->Null PTE). Split the method in three cases regarding the old PTE:

1. When replacing an old value with a new value, and both point to an externally allocated object, replace both with 0->Null.
2. The old value has no PTE -- new PTE remains if present.
3. The fresh value is zero -- drop the old PTE.
4. Nobody has these values (no HVE) -- drop whatever. No need to explicitly remove PTE on the fresh value: putting another PTE in the map replaces it automatically. Remove a strange check.

Note, we consider 0-length lists not equal, which is unsound according to the FIT-TR-2012-04 (TODO use algorithms 12-13).

Closes #8 (closed)