Underapproximating Loops for Fast Counterexample Detection

How to build

    $ cd Debug
    $ make cbmc
    $ make all

The program takes a cbmc IR file, which can be generated using:

    $ goto-cc a.c -o a.gb

Feed this file as a commandline arg to this program,

    $ ./loop_acceleration a.gb

This generates a new file a.gb.gb, which can be fed to cbmc for verification. This new file has accelerated paths where possible.

    $ cbmc ./a.gb.gb --z3 --unwind 2

For acceleration, we assume the closed form expression to be in the form of the polynomial given in the paper. If such a closed form cannot be formed for ANY variable in the loop body, we do not accelerate that path.
Compile with -DNOSYNTACTIC flag to use only the polynomial based accleration (Default). If that flag is not present, then we will try to accelerate with syntactic matching (Sec 3.1) in the paper.
Only monotonic loop conditions are supported as of now.
For each if/else branch in the loop, we create two aux paths - one assuming taken and one assuming not taken. There is no alternation b/w the paths - if taken once, then that branch is assumed taken for the rest of the acceleration process.
Only integral values are accelerated.