For some tests duplicate and/or missing declarations involving arrays cause problems in incremental smt2 decision procedure

[thomasspriggs]

For some tests duplicate and/or missing declarations involving arrays cause problems in incremental smt2 decision procedure. This needs further investigation to debug. This is known to affect the following tests -

• cbmc/byte_extract1/test.desc
• cbmc/Initialization6/test.desc
• cbmc/Pointer_byte_extract4/program-only.desc
• cbmc/Pointer_byte_extract4/test.desc

The errors reported include -

SMT solver returned an error message - line 32 column 56: unknown constant main::1::x!0@1#1
SMT solver returned an error message - line 29 column 59: invalid declaration, constant 'main::1::outlist!0@1#1[[0]]' (with the given signature) already declared
SMT solver returned an error message - line 27 column 106: named expression already defined
SMT solver returned an error message - line 27 column 106: named expression already defined