Unexpected behavior where bi-unroll limit is used as branching limit

[2over12]

Was messing around with ACT on a simple example:

#include <stdlib.h>

int f(int i) {
    int* x = malloc(sizeof(int));
    if (i < 3) {
        free(x);
    }
    return *x; 
}

int g() {
    return f(2);
}

With default options this dumps no specs: esy x gillian-c act /tmp/t.c --specs-to-stdout -l verbose --reporters="file"

I realized this is because bi-unroll is also tied to the max branching factor which seems odd and unexpected to me: https://github.com/GillianPlatform/Gillian/blob/500b9069a64bfd5175f6ff8de522db29112ef72d/GillianCore/command_line/act_console.ml#L146

Is there any reason not to just have its own parameter?

[giltho]

Hello, I'm so sorry for the late reply, there was the PLDI panic and then it slipped my mind

The name bi_unroll_depth is misleading indeed, it's actually implemented by capping the allowed number of branches. This is not the best heuristics for bounding bi-abduction, but it is sound. Implementing another heuristics would require deeper reworking that is not at the top of our priority list for now :(