Find inputs to a function which break the postcondition on the output

Question

I have a function in a programming language, e.g. C. I require the output of the function to meet a certain condition. If there is some input to this function for which the output does not meet the required condition, I need to find any such exact input.

I need to do this in general, but for rather simple functions, e.g. the number of the loops is fixed and does not depend on the input. Another requirement is that I need to do this very fast. I found that CBMC tool [https://www.cprover.org/cbmc/] may help me, but I am not sure how to use it. I also welcome solutions which convert the problem into the CNF formula (but I still need to retrieve the counterexample input).

An example of the function:

int function(int n) {
    int m = 0;
    for(int i = 1; i < 8; i++) {
        m += n*i;
    }
    int output = m % 11;
    return output;
}
// POSTCONDITION: require the output < 10 for all inputs
// VERIFICATION: this is not true, the counterexample is the input n=9.

Answer 1

Consider this simple function with no loops at all:

bool function (int a, int b, int c)
{
   bool answer = a*a*a + b*b*b + c*c*c != 42;
   // POSTCONDITION: require answer==true
}

It took a few hundred computer-years (or, in real time, a couple of weeks on a 500,000-strong grid of PCs) to discover that there is a counterexample (pdf):

(−80538738812075974)³ + 80435758145817515³ + 12602123297335631³ = 42

A program that can do that very fast is a very, very good program indeed.