cannot generate inv from Timos & Ferhat about dig HOT 2 CLOSED

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

void vassume(int b) {}
void vtrace(int g, int h, int x, int y) {}
void vtrace1(int f_x_f_x, int f_y_f_x, int f_y_f_y, int f_x1_f_x2) {}

// f(x) = x(x + 1)
int F(int x) { return x * x; }

void mainQ(int x1, int x2) {
  vassume(-20 < x1); vassume(x1 < 20);
  vassume(-20 < x2); vassume(x2 < 20);
  
  int x = x1 + x2;
  int y = x1 - x2;
  int f_x = F(x);
  int f_y = F(y);
  int f_x1 = F(x1);
  int f_x2 = F(x2);

  int myg = f_x*f_x - 2*f_y*f_x + f_y*f_y;
  int myh = f_x1*f_x2;
  vtrace(myg, myh, x, y); // <--------------------------HERE


  int f_x_f_x = f_x*f_x;
  int f_y_f_x = f_y*f_x;
  int f_y_f_y = f_y*f_y;
  int f_x1_f_x2 = f_x1*f_x2;

  vtrace1(f_x_f_x,f_y_f_x,f_y_f_y,f_x1_f_x2);
}

void main(int argc, char *argv[]) {
  mainQ(atoi(argv[1]), atoi(argv[2]));
}

tnguyen@DynaROARS ~/g/d/src (dev)> time ~/miniconda3/bin/python3 -O dig.py  ../tests/t2.c --maxdeg 1 --noss --noieq --nocong --nominmax                                               (base) 
settings:INFO:2023-05-22 13:54:58.882998: dig.py ../tests/t2.c --maxdeg 1 --noss --noieq --nocong --nominmax
alg:INFO:analyzing '../tests/t2.c'
alg:INFO:analyzing '../tests/t2.c'
alg:INFO:got 152 traces over 2 locs
alg:INFO:check 2 invs using 152 traces (0.03s)
alg:INFO:simplify 2 invs (0.01s)
tmpdir: /var/tmp/dig_2029142113675619442_wwoafspq
vtrace (1 invs):
1. -g + 16*h == 0
vtrace1 (1 invs):
1. 16*f_x1_f_x2 - f_x_f_x + 2*f_y_f_x - f_y_f_y == 0