Project

General

Profile

To do #9433

strong itp-lra-algorithm generates redundant formula

Added by Sepideh Asadi 5 months ago.

Status:
New
Priority:
Normal
Assignee:
Start date:
28/11/2018
Due date:
% Done:

0%

Estimated time:

Description

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

Also available in: Atom PDF