CN: Multiplication overflow check slow

[lwli11]

This check against multiplication overflow seems very slow as well. Any ideas how to speed this up?

#include <limits.h>
int test(int a, int b){
        if (a > 0 && b>0 && INT_MAX / b > a){
                return a*b;
        }
        return 0;
}

 

time cn verify mult_overflow.c
[1/1]: test -- pass

real    11m30.198s

[lwli11]

And checking all possible conditions:

real 70m27.931s
user 0m0.197s
sys 0m0.080s

#include <limits.h>
int test(int a, int b){
        if (a==0 || b==0){
                return 0;
        }
        else if (a > 0 && b>0 && INT_MAX / b > a){
                return a*b;
        }
        else if (a>0 && b <0 && b > INT_MIN/a){
                return a*b;
        }
        else if (a<0 && b>0 && a > INT_MIN / b){
                return a*b;
        }
        else if (a<0 && b<0 && b > INT_MAX / a){
                return a*b;
        }
        return 0;
}

[septract]

These both seem to be sending queries to the solver that it is hanging on for a long time.

The first is a bit quicker with --solver-type=cvc5 - a couple of minutes on my Macbook. The second is very slow with CVC5.