hifrog

investigate LRA strong itp Alg and compare the result with weak one; it seems weak mode generates compact and good summary, the same as TACAS version, but STRONG mode contains some redundant parts in the formula.

------------------------------------------
example:
short get_nondet_short();

int abs(int x) {
return x >= 0 ? x : -x;
}

int main() {
int x = get_nondet_short();
x = abs(x);
int y = x + 2;
assert(y >= 0);
}

------------------------------------------
How to run?

weak:
./hifrog --logic qflra --itp-lra-algorithm 2 example.c

strong:
./hifrog --logic qflra --itp-lra-algorithm 0 example.c