Generate invariants for C programs with the functions from math.h about dig HOT 3 CLOSED

#include <stdio.h>
#include <stdlib.h>

void vassume(int b){}
void vtrace(int x, int y){} 

void mainQ( ) 
{
  int x,y;  
  x=0;
  y=0;
  vassume (x==0&&y==0);  
  while(x<=100)
    {// loop invariant:x==y
      vtrace(x,y);
      y=y+1;
      x=x+1;
    } 
    //assert(x==y);
}

void main(int argc, char **argv){
    mainQ();
}

sage -python -O dig.py bench16_potsumm1.c -log 3 -nominmax -nominmaxplus -nomp -maxdeg 5 -seed 2
settings:INFO:2021-07-02 15:25:23.002700: dig.py bench16_potsumm1.c -log 3 -nominmax -nominmaxplus -nomp -maxdeg 5 -seed 2
alg:INFO:analyze '/home/ly/Music/benchmark-tasep/bench16_potsumm1.c'
alg:INFO:compute symbolic states (4.63s)
alg:INFO:infer invs at 1 locs: vtrace
alg:INFO:found 1 eqts (1.41s)
alg:INFO:found 5 ieqs (0.12s)
alg:INFO:test 6 invs using 101 traces (0.02s)
alg:INFO:simplify 6 invs (0.04s)
* prog bench16_potsumm1 locs 1;  invs 4 (Eqt: 1, Oct: 3) V 2 T 2 D 1;  NL 0 (1) ;
-> time eqts 1.4s, ieqs 0.1s, simplify 0.1s, symbolic_states 4.6s, total 6.2s
-> checks  0 () change depths 0 () change vals 0 ()
-> max  0 () change depths 0 ()
runs 1
rand seed 2.0, test (11, 57)
vtrace (4 invs):
1. x - y == 0
2. -y <= 0
3. x - y <= 0
4. -x + y <= 0
tmpdir: /var/tmp/dig_2_lke27k9i