Drop symbolic path domain

[viktormalik]

Originally, symbolic paths were meant to handle the situation when a heap invariant containing addresses of dynamic objects would be used for cases when the dynamic objects were not allocated.

Thanks to the new dynamic object management class, this problem can be solved in a better way by adding a loop guard (guarding the object allocation) directly to the heap invariant. In particular, if a heap template row value contains a pointer-object equality (stating that the pointer may point to the object), this adds (conjuncts) a loop-select guard of the object allocation loop.

For example, if the original row value was e.g.:

p#lb50 == &dynamic_object$16 || p#lb50 == &dynamic_object$32

where dynamic_object$16 is allocated in a loop with $guard#ls30 and dynamic_object$32 is allocated in a loop with $guard#ls50, the new row value is:

(p#lb50 == &dynamic_object$16 && $guard#ls30) || (p#lb50 == &dynamic_object$32 && $guard#ls50)

This makes sure that invariants for the dynamic object are used only if the objects were actually allocated.

This new approach brings some considerable speedup, e.g. for the heap-data regression suite:

<master> $ time make test
real    0m48.871s
user    0m48.118s
sys 0m0.510s

<drop-sympath-domain> $ time make test
real    0m12.895s
user    0m12.416s
sys 0m0.352s