--paths fails on some regression/cbmc benchmarks

[peterschrammel]

Running develop (8900b60) --paths lifo now on regression/cbmc:

• Bitfields3 crashes
• Multi_Dimensional_Array6 doesn't terminate or takes very long
• address_space_size_limit1 doesn't terminate or takes very long
• array-tests doesn't terminate or takes very long
• coverage_report1 crashes
• gcc_switch_case_range1 fails
• gcc_switch_case_range2 fails
• havoc_object1 fails

[tautschnig]

I believe it was 8fb2902 (#3433) that broke this. The counters must be kept across instances of goto_symext as otherwise multiple objects with the same name, but different types, exist.

[tautschnig]

What I just posted only affects Bitfields3, the issues with the others are different (in parts only issues with the *.desc files).

[tautschnig]

See #3959 for the first bugfix.

[tautschnig]

#3960 addresses gcc_switch_case_range1, gcc_switch_case_range2, havoc_object1.

[tautschnig]

The number of paths in array-tests will inevitably mean that single-path symbolic execution takes a very long time.

[tautschnig]

Each loop iteration in address_space_size_limit1 introduces a number of branches (in malloc), which induces a large number of paths, and thus single-path symbolic execution will take a very long time.

[tautschnig]

Multi_Dimensional_Array6 does seem to terminate with --unwind 1, --unwind 2, and might just take very long for --unwind 3 (or any higher bound) given the number of paths that the nested and sequenced loops introduce.

[tautschnig]

And finally #3961 for coverage-report1.