Regression issues with Z3

[rafaelsamenezes]

Just to keep track of tests that are not working;

From esbmc core:

• [ ] 01_cbmc_Pointer14: Segmentation Fault while building error trace
• [ ] 01_cbmc_Malloc18: Segmentation Fault while building error trace
• [ ] 01_cbmc_String_Abstraction6: Unimplemented type'd expression (7) in smt get
• [ ] 01_cbmc_Structs1: Segmentation Fault while building error trace
• [ ] 02eureka02: Sorts (Array ( BitVec 64) ( BitVec 32)) and (Array ( BitVec 3) (_ BitVec 32)) are incompatible
• [ ] 02eureka21: Sorts (Array ( BitVec 64) ( BitVec 32)) and (Array ( BitVec 3) (_ BitVec 32)) are incompatible
• [ ] 10_bicycle_02: Segmentation Fault while building error trace
• [ ] 33_s3_srvr_blast_04: Segmentation Fault while building error trace
• [ ] github_154: Segmentation Fault while building error trace

This is not a comprehensive list

Also, some testcases that are instantly solved by boolector don't get solved.

For now, I think we should mark all tests that are not instantly solved as THROROUGH (with no default solver) and the others as KNOWNBUG (forcing the use of z3)

UPDATE:

Some tests e.g llvm/variadic_function don't work on boolector but do on Z3

[github-actions[bot]]

Stale issue message

[lucasccordeiro]

@rafaelsamenezes: Is this issue still valid?

[lucasccordeiro]

@rafaelsamenezes: Is this issue still valid?