Assert failure in hflmc2_refine.ml

[kamocyc]

Input:

%HES
Sentry  =ν exi_x196 < 1 || Exists exi_x196.
Exists exi_x217 =ν
  (exi_r278 < 1
    || exi_r278 < 1 * exi_x217 || exi_r278 < -1 * exi_x217 || F_0_ff_ap_ exi_x217 exi_r278
    || exi_r279 < 1
      || exi_r279 < 1 * -exi_x217 || exi_r279 < -1 * -exi_x217 || F_0_ff_ap_ (-exi_x217) exi_r279
      || Exists (exi_x217 - 1))
  && exi_x217 >= 0.
F_0_tt x2210 =ν
  exi_r2311 < 1 || exi_r2311 < 1 * x2210 || exi_r2311 < -1 * x2210 || F_0_tt_ap_ x2210 exi_r2311.
F_0_tt_ap_ x2412 exi_r2513 =ν
  ((x2412 >= 0
    && rec_G_1_ff_13214 < 1 + 1 * exi_r2513
        || rec_G_1_ff_13214 < 1 + -1 * exi_r2513
          || rec_G_1_ff_13214 < 1 + 1 * (x2412 - 1)
              || rec_G_1_ff_13214 < 1 + -1 * (x2412 - 1)
                || rec_G_1_ff_13214 < 1 || G_1_ff_1 rec_G_1_ff_13214 (x2412 - 1) exi_r2513
    || x2412 < 0 && exi_r2513 = 5)
    && F_0_tt exi_r2513
    || (x2412 >= 0
        && rec_G_1_ff_13215 < 1 + 1 * -exi_r2513
          || rec_G_1_ff_13215 < 1 + -1 * -exi_r2513
              || rec_G_1_ff_13215 < 1 + 1 * (x2412 - 1)
                || rec_G_1_ff_13215 < 1 + -1 * (x2412 - 1)
                    || rec_G_1_ff_13215 < 1 || G_1_ff_1 rec_G_1_ff_13215 (x2412 - 1) (-exi_r2513)
        || x2412 < 0 && -exi_r2513 = 5)
      && F_0_tt (-exi_r2513)
      || F_0_tt_ap_ x2412 (exi_r2513 - 1))
  && exi_r2513 >= 0.
F_0_ff_ap_ x2816 exi_r2917 =ν
  ((x2816 >= 0
    && rec_G_1_ff_13218 < 1 + 1 * exi_r2917
        || rec_G_1_ff_13218 < 1 + -1 * exi_r2917
          || rec_G_1_ff_13218 < 1 + 1 * (x2816 - 1)
              || rec_G_1_ff_13218 < 1 + -1 * (x2816 - 1)
                || rec_G_1_ff_13218 < 1 || G_1_ff_1 rec_G_1_ff_13218 (x2816 - 1) exi_r2917
    || x2816 < 0 && exi_r2917 = 5)
    && F_0_tt exi_r2917
    || (x2816 >= 0
        && rec_G_1_ff_13219 < 1 + 1 * -exi_r2917
          || rec_G_1_ff_13219 < 1 + -1 * -exi_r2917
              || rec_G_1_ff_13219 < 1 + 1 * (x2816 - 1)
                || rec_G_1_ff_13219 < 1 + -1 * (x2816 - 1)
                    || rec_G_1_ff_13219 < 1 || G_1_ff_1 rec_G_1_ff_13219 (x2816 - 1) (-exi_r2917)
        || x2816 < 0 && -exi_r2917 = 5)
      && F_0_tt (-exi_r2917)
      || F_0_ff_ap_ x2816 (exi_r2917 - 1))
  && exi_r2917 >= 0.
G_1_ff_1 rec_G_1_ff_13320 x3421 r3522 =ν
  rec_G_1_ff_13320 > 0
  && (x3421 >= 0 && G_1_ff_1 (rec_G_1_ff_13320 - 1) (x3421 - 1) r3522 || x3421 < 0 && r3522 = 5).

Running hflmc2 input.hes gives me the error below:

Uncaught exception:
  
  "Assert_failure lib/refine/hflmc2_refine.ml:408:34"

Raised at file "lib/refine/hflmc2_refine.ml", line 408, characters 34-46
Called from file "src/list.ml", line 325, characters 13-17
Called from file "src/list.ml", line 557, characters 34-40
Called from file "lib/refine/hflmc2_refine.ml", line 405, characters 22-275
Called from file "lib/refine/hflmc2_refine.ml", line 340, characters 16-46
Called from file "lib/refine/hflmc2_refine.ml", line 340, characters 16-46
Called from file "lib/refine/hflmc2_refine.ml", line 340, characters 16-46
Called from file "lib/refine/hflmc2_refine.ml", line 353, characters 51-81
Called from file "lib/refine/hflmc2_refine.ml", line 369, characters 31-44
Called from file "lib/refine/hflmc2_refine.ml", line 12, characters 10-14
Called from file "lib/refine/traceVar.ml", line 67, characters 10-14
Called from file "lib/refine/hflmc2_refine.ml", line 350, characters 20-1023
Called from file "lib/refine/hflmc2_refine.ml", line 340, characters 16-46
Called from file "lib/refine/hflmc2_refine.ml", line 340, characters 16-46
Called from file "lib/refine/hflmc2_refine.ml", line 340, characters 16-46
Called from file "lib/refine/hflmc2_refine.ml", line 568, characters 18-76
Called from file "lib/refine/hflmc2_refine.ml", line 340, characters 16-46
Called from file "lib/refine/hflmc2_refine.ml", line 568, characters 18-76
Called from file "lib/refine/hflmc2_refine.ml", line 590, characters 11-58
Called from file "lib/refine/hflmc2_refine.ml", line 606, characters 39-57
Called from file "lib/hflmc2.ml", line 28, characters 15-19
Called from file "lib/hflmc2.ml", line 40, characters 16-30
Called from file "lib/hflmc2.ml", line 146, characters 24-101
Called from file "lib/hflmc2.ml", line 177, characters 4-52
Called from file "bin/main.ml", line 14, characters 16-32

[Hogeyama]

This error is due to the free variables (exi_r278 in Exists, for example), which is not allowed.
(hflmc2 accepts free variables only in the main function. This may look weird but is needed for compatibility with hflmc)

I'll improve the error message. Thanks.