Using /di flag it seems causes an assertion violation to be missed

[zvonimir]

It is SVCOMP time of year :), and hence we are plowing through various issues as we encounter them.
See the attached file: pump.txt
When I run it with:

corral pump.bpl /tryCTrace /noTraceOnDisk /printDataValues:1 /k:1 /useProverEvaluate /timeLimit:1200 /cex:1 /maxStaticLoopBound:1 /recursionBound:1024

I get an error trace really fast.
When I add /di flag, the error is not found, and in fact it seems that it gets missed (I run it until 200+ unrollings and it was still not found):

corral pump.bpl /tryCTrace /noTraceOnDisk /printDataValues:1 /k:1 /useProverEvaluate /timeLimit:1200 /cex:1 /maxStaticLoopBound:1 /recursionBound:1024 /di

I also see warnings of this form, not sure if those matter at all:

WARNING: Duplicate si_unique_call annotations in test_loop_$bb1

Anyhow, I just wanted to report a potential soundness bug. Oh, and finally this example almost certianly does contain an assertion violation.