This reverts commit 4cb07686.

Not only if  we give up extending it or we prove it is safe.
This way, we store all sequences that we ever create.

This reverts commit 62d66147.

That commit breaks things, we need to solve it better.

Do not keep those that are surely unreachable.

Concrete bool has not rewrite_and_simplify() method.

We must substract 1.

A step to soundness again.

And infer more of them.

We can reduce only equalities atm...

We cannot rewrite exprs with assuming exprs...

This reverts commit 0d4254eb.
This was wrong, it worked well.

We didn't finish the lhs transformation before
replacing the rest of the formula.

There it can happen, that we do not match all inputs
and we fail on assertions.

If found that it holds in more consecutive states.

This test was on the edge...

Re-use the overapprox_state method that we already have.

Do not generate relations for pre-prestates, just check whether the
already generated relations for pre-state hold.

Do not create a set if it is already a set.

To filter out the relations that are not definitely useful.

No functional changes.