OpenSMT 2

Happens when running all the claims at once. When running this benchmarks one claim after another (3 runs instead of 1), then there is no problem
Code example: /hi-bench/main-bench/funfrog_regression/05_McMillan/diskperf.cil_loopfree.c

Output:
; ============================[ Search Statistics ]==============================
; | Conflicts | ORIGINAL | LEARNT | Progress |
; | | Vars Clauses Literals | Limit Clauses Lit/Cl | |
; ===============================================================================
; 0 | 0 0 | 53.660 s | 369.918 MB
SOLVER TIME: 54.877
UNSAT - it holds!
ASSERTION IS TRUE
Start generating interpolants...

1. Proof graph building begin
2. Memory used before building the proof: 371.594 MB
3. (1) Empty clause given in input or generated at preprocessing time: single node proof
4. Number of nodes: 1 (leaves: 0 - learnt: 0 - derived: 0 - theory: 0)
5. Maximum, average size of leaves: 0 -nan
6. Maximum, average size of learnt: 0 -nan
7. Number of edges: 0
8. Number of distinct variables in the proof: 0
9. Memory used after building the proof: 371.941 MB
10. Proof graph building end
11. Single interpolant
12. Using Pudlak for propositional interpolation
    evolcheck: PGInterAux.C:210: opensmt::icolor_t ProofGraph::getClauseColor(const ipartitions_t&, const ipartitions_t&): Assertion `clause_in_A || clause_in_B' failed.
    Aborted (core dumped)