incomplete: sea*

[chkl]

0dd0cf3e2afd5800092cd35de9d35592c50519a2 (c/loop-new/gauss_sum_true-unreach-call_true-termination.i)

void __DUMMY_VERIFIER_error()
{
}
void __DUMMY_VERIFIER_assert(int condition)
{
}
extern void __VERIFIER_error(void);
extern void __VERIFIER_assume(int);
void __VERIFIER_assert(int cond)
{
    if (!cond)
    {
    ERROR:
        __VERIFIER_error();
    }
    return;
}
int __VERIFIER_nondet_int();
int main()
{
    int n, sum, i;
    n = __VERIFIER_nondet_int();
    if (!(1 <= n && n <= 1000))
    {
        return 0;
    }
    sum = 0;
    for (i = 1; i <= n; i++)
    {
        sum = sum + i;
    }
    __VERIFIER_assert(n * (n + 1) != 0);
    __DUMMY_VERIFIER_assert(2 * sum == n * (n + 1));
    return 0;
}

[chkl]

minimal:

extern void __VERIFIER_error(void);

void __VERIFIER_assert(int cond)
{
    if (!cond)
    {
    ERROR:
        __VERIFIER_error();
    }
    return;
}
int __VERIFIER_nondet_int();
int main()
{
    int n;
    n = __VERIFIER_nondet_int();
    if (!(1 <= n && n <= 1000))
    {
        return 0;
    }

    __VERIFIER_assert(n * (n + 1) != 0);
    return 0;
}