search

ChenfengWei0 / esbmc

The efficient SMT-based bounded model checker
http://esbmc.org/
Other
0 stars 1 forks source link

k-induction-2 #7

Open ChenfengWei0 opened 1 year ago

ChenfengWei0 commented 1 year ago 
#include <stdio.h>

int x;
int y;
void moveLeftUp()
{
    --x;
    ++y;
}

void moveLeftDown()
{
    --x;
    --y;
}

void moveRightUp()
{
    ++x;
    ++y;
}

void moveRightDown()
{
    ++x;
    --y;
}

int main()
{
    x = 0;
    y = 0;
    while (nondet_int())
    {
        if (nondet_int())
        {
            moveLeftUp();
        }
        if (nondet_int())
        {
            moveLeftDown();
        }
        if (nondet_int())
        {
            moveRightUp();
        }
        if (nondet_int())
        {
            moveRightDown();
        }
        if (nondet_int())
        {
            assert((x + y) % 2 == 0);
        }
        if (nondet_int())
        {
            assert(!(x == 2 && y == 4));
        }
    }
}

ok

ChenfengWei0 commented 1 year ago 
#include <stdio.h>

int x;
int y;
void moveLeftUp()
{
    --x;
    ++y;
}

void moveLeftDown()
{
    --x;
    --y;
}

void moveRightUp()
{
    ++x;
    ++y;
}

void moveRightDown()
{
    ++x;
    --y;
}

int main()
{
    x = 0;
    y = 0;
    while (nondet_int())
    {
        if (nondet_int())
        {
            moveLeftUp();
        }
        if (nondet_int())
        {
            moveLeftDown();
        }
        if (nondet_int())
        {
            moveRightUp();
        }
        if (nondet_int())
        {
            moveRightDown();
        }
    }
    assert((x + y) % 2 == 0);  
    assert(!(x == 2 && y == 4)); // if comment this one not ok, otherwise ok
}