EXPL_PRED_STMT and EXPL_PRED_SPLIT domain for XCFA

[mondokm]

EXPL_PRED_STMT is similar to EXPL with StmtApplier and maxenum=1 combined with PRED_CART
EXPL_PRED_SPLIT is EXPL combined with PRED_SPLIT

At the start everything is tracked using predicates, but if a variable appears in an atom inside an interpolant together with a previously unseen operand, we start tracking it explicitly in order to avoid counting using predicates.

[leventeBajczi]

Thanks, I think this is great! I left a few comments here-and-there, but all in all, I'm happy to approve. If you think it's beneficial, feel free to address my comments.

Have you run any comprehensive tests/benchmarks to see how this behaves?

[github-actions]

Benchexec test report for a selection of SV-Benchmarks (correct / incorrect / all):

Rundefinition	BOUNDED	CEGAR	HORN
SV-COMP25_no-data-race	✅ (13 / 0 / 49) HTML/CSV	✅ (33 / 0 / 48) HTML/CSV	✅ (13 / 0 / 49) HTML/CSV
SV-COMP25_no-overflow	❓ (0 / 0 / 1024) HTML/CSV	✅ (44 / 0 / 951) HTML/CSV	❓ (0 / 0 / 981) HTML/CSV
SV-COMP25_termination	❗ (7 / 2 / 283) HTML/CSV	❓ (0 / 0 / 558) HTML/CSV	✅ (4 / 0 / 277) HTML/CSV
SV-COMP25_unreach-call	❗ (16 / 1 / 594) HTML/CSV	❗ (87 / 1 / 435) HTML/CSV	❗ (34 / 1 / 569) HTML/CSV
SV-COMP25_valid-memcleanup	❓ (0 / 0 / 65) HTML/CSV	❓ (0 / 0 / 65) HTML/CSV	❓ (0 / 0 / 65) HTML/CSV
SV-COMP25_valid-memsafety	✅ (1 / 0 / 1418) HTML/CSV	❗ (30 / 2 / 999) HTML/CSV	✅ (1 / 0 / 1496) HTML/CSV