[Question]Soft Constraints for Irrelevant Variables in Test Suite Exploration

[kosuke321]

I would like to set irrelevant variables to values such as 0 during test suite exploration.
Is there a way to apply soft constraints on variables in CBMC?

If there are any alternative solutions, I would appreciate your suggestions as well.

[tautschnig]

Would assumptions be what you are looking for? See https://diffblue.github.io/cbmc/cprover-manual/md_modeling-assumptions.html. If your problem cannot be solved using assumptions, would you be able to elaborate upon your question by proving a short example?

[kosuke321]

I would like to explore a test suite to achieve full branch coverage for the following code, but I want to set unrelated input values to 0 as much as possible.

void target(int a, int b, int c) {

    if(a < 10 && b < 20){
        return 0;
    }

    if(a == b && c == 20){
        return -1;
    }
    return c;
}

int main(void){
    int x, y, z;
    __CPROVER_input("x", x);
    __CPROVER_input("y", y);
    __CPROVER_input("z", z);

    target(x, y, z);

    return 0;
}

For the test suite covering the first if statement, since the argument c (input z) is not related, I would like it to be set to 0 as much as possible.

On the other hand, for the second if statement, since c is involved, I want to explore test cases that satisfy coverage by varying the value of c (input z).

However, for each test suite, I do not know in advance which variables are unrelated inputs, so if I use assumptions and they are incorrect, there is a high possibility that the test suite cannot be found.

Therefore, I would like to know if there is a way to apply variable constraints as much as possible.