synthesis test 7

[polgreen]

Test-synthesis-7 seems to time out, we should check the encoding is as expected:

/** This is an example to test UCLID5's invariant synthesis.
  */

module main
{
  synthesis function h(x : integer, y : integer) : boolean;
  var x, y, z : integer;
  
  init {
    assume (x == 0);
    assume (y == 1);
    assume (z == 2);
  }
  
  next {
    /*
    x' = x + 1;
    y' = x + y;
    z' = y + z;
    */
    havoc x;
    havoc y;
    havoc z;
    assume (x' == x + 1);
    assume (y' == x + y);
    assume (z' == y + z);
    assert (z >= 0);
  }
  
  invariant always_positive: (z >= 0) && h(z, y);
  
  control {
    induction;
    check;
    print_results;
  }
}