<p>Consider this simple function with no loops at all:</p>
<pre><code>bool function (int a, int b, int c)
{
   bool answer = a*a*a + b*b*b + c*c*c != 42;
   // POSTCONDITION: require answer==true
}
</code></pre>
<p>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 <a href="https://arxiv.org/pdf/2007.01209.pdf" rel="nofollow noreferrer">counterexample</a> (pdf):</p>
<blockquote>
<p>(−80538738812075974)<sup>3</sup> + 80435758145817515<sup>3</sup> + 12602123297335631<sup>3</sup> = 42</p>
</blockquote>
<p>A program that can do that very fast is a very, very good program indeed.</p>
Find inputs to a function which break the postcondition on the output
<p>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.</p>
<p>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).</p>
<p>An example of the function:</p>
<pre><code>int function(int n) {
    int m = 0;
    for(int i = 1; i &lt; 8; i++) {
        m += n*i;
    }
    int output = m % 11;
    return output;
}
// POSTCONDITION: require the output &lt; 10 for all inputs
// VERIFICATION: this is not true, the counterexample is the input n=9.
</code></pre>