// S : tags   c sym  $TAGS
// S : expect --result valid
// S : cc     -o test.bc  $CC_OPT $file
// S : verify --symbolic --solver $solver --sequential -o nofail:malloc $V_OPT test.bc

// N : V         : CC_OPT      : V_OPT : TAGS : RESULT
// V : big.100   : -DNUM=100   :       : big  : valid
// V : big.1000  : -DNUM=1000  :       : big  : valid
// V : small.5   : -DNUM=5     :       : big  : valid
// V : big.46340 : -DNUM=46340 :       : big  : valid

extern void __VERIFIER_error() __attribute__ ((__noreturn__));

/*
 * Recursive implementation of prime number test
 * (Sieve of Eratosthenes)
 *
 * Author: Jan Leike
 * Date: 2013-07-17
 *
 */

extern int __VERIFIER_nondet_int(void);

// Multiplies two integers n and m
int mult(int n, int m) {
    if (m < 0) {
        return mult(n, -m);
    }
    if (m == 0) {
        return 0;
    }
    if (m == 1) {
        return 1;
    }
    return n + mult(n, m - 1);
}

// Is n a multiple of m?
int multiple_of(int n, int m) {
    if (m < 0) {
        return multiple_of(n, -m);
    }
    if (n < 0) {
        return multiple_of(-n, m); // false
    }
    if (m == 0) {
        return 0; // false
    }
    if (n == 0) {
        return 1; // true
    }
    return multiple_of(n - m, m);
}

int is_prime_(int n, int m);
int is_prime(int n);

// Is n prime?
int is_prime(int n) {
    return is_prime_(n, n - 1);
}

int is_prime_(int n, int m) {
    if (n <= 1) {
        return 0; // false
    }
    if (n == 2) {
        return 1; // true
    }
    if (n > 2) {
        if (m <= 1) {
            return 1; // true
        } else {
            if (multiple_of(n, m) == 0) {
                return 0; // false
            }
            return is_prime_(n, m - 1);
        }
    }
}

int main() {
    int n = __VERIFIER_nondet_int();
    if (n < 1 || n > NUM) {
        // additional branch to avoid undefined behavior
        // (because of signed integer overflow)
        return 0;
    }
    int result = is_prime(n);
    int f1 = __VERIFIER_nondet_int();
    if (f1 < 1 || f1 > NUM) {
        // additional branch to avoid undefined behavior
        // (because of signed integer overflow)
        return 0;
    }
    int f2 = __VERIFIER_nondet_int();
    if (f2 < 1 || f2 > NUM) {
        // additional branch to avoid undefined behavior
        // (because of signed integer overflow)
        return 0;
    }

    if (result == 1 && mult(f1, f2) == n && f1 > 1 && f2 > 1) {
        ERROR: __VERIFIER_error();
    } else {
        return 0;
    }
}