(*) When you had condition on two consecutive lines, the output
was screwed-up.

Merge branch 'arithmetic-generation' of ssh://pajda.fit.vutbr.cz/ifiedortom/forester-resource-bounds into arithmetic-generation

LargeBlockFunctors: Fix the issue with AllPaths when w ==x in shape
  and this led to incorrect rule applied;
termination: fix issue with optimization.

termination: IF there exist some reachable symbolic reset and some other
   reset, we change it to the symbolic one (*).

 (*) This is done to circumvent some strange Loopus behaviour, which is
 probably not as easy to patch in Loopus, after discussion with Moritz.

LargeBlockFunctors: Add limitation of the analysis to reachable stuff.

Prover: Freed variables are now considered as "decreases".

compiler: reduce the number of variables in shapes;
Prover: fix assert issue.

LargeBlockFunctors: Add resets to infinity;
NormChangeGraph: Add guard so nothing is fucked up.

various: Minor speed optimization;
bench: updated benchmarks to support some stuff;
bench: add simplified skip-lists.

Condition: Add simplified version of Condition for Arithmetic Generation;
Loop: Fix issue with Loop successors and summaries;
Loop: Add collection of all conditions within the loop;
termination: fix issues with injected conditions.

LargeBlockFunctors: Add missing reset for malloc();
NormChangeGraph: Add pruning of dominated rests;
NormChangeGraph: Add more precise location in reseted norms;
NormList: Add location for the NormSet;
termination: Add pruning for norms, that do not reach the location.