Example for improvement of guard simplification

[martin-cs]

Supporting material for feature request : not bug.

@tautschnig I remember we talked ages ago about improving the simplification of guard expressions (to help a problem Pascal was having with switch). It seems that:

sv-benchmarks/c/recursive-simple/id_o1000_false-unreach-call.c

(from SV-COMP) gives a good example of guards that look like they should be simplifable.

[tautschnig]

@martin-cs If you've got the time to give this SV-COMP example a try with #310 applied that would be good to gather feedback. I've been using those bdd patches for quite a while.

[martin-cs]

Have done and that does indeed simplify things. Most appreciated.

[tautschnig]

Might need some poke so as to get #310 merged then...

[tautschnig]

Though there is room for even further improvement by using bddt in simplify_exprt::simplify_boolean.

[peterschrammel]

Requested feature has been implemented.