Linear Two Variable Equality Domain Refining Value Domain

[DrMichaelPetter]

In this PR, lin2vareq interprets inequality guards as opportunities to refine value domains beyond the syntactical obvious intersection with bounds. Check the following example:

int x, y, z;
x = 3*y + 1; // a
z = 5*x + 7; // b
if (x>0) {
  __goblint_check( x >  0 );
  __goblint_check( y > -1 ); // A
  __goblint_check( z >  7 ); // B
}

Invariants A and B can assumed to hold due to assignments a and b establishing relations. Both invariants can not be tracked via value analysis.

[DrMichaelPetter]

Preliminary results look already promising, even on a 2GB 5min run. I still have to sort out some bugs in the svcomp-runs, so maybe it will become even better.

[sim642]

As I've mentioned before, it might be worth looking into using this in the termination categories. I cannot immediately name SV-COMP termination tasks where we thought equalities between program variables and our loop counters would be useful, but it shouldn't be too hard to construct or find small examples from sv-benchmarks that we cannot handle.

Our SV-COMP autotuner uses Apron polyhedra, so maybe it's not properly benefiting from these 2-variable things. That's also worth checking out.