Incorrect result from satisfiability test

[cirodrig]

The set {[x, y] : 0 <= x <= 4 && 0 <= y <= 4 && 4y < 5x && 9x <= 8y} is empty, but is_upper_bound_satisfiable() returns a nonzero value. Emptiness can be verified by enumerating and testing all points in the range. Furthermore, the library prints the set's characteristic function as FALSE.

The following complete program reproduces the problem.

#include <stdio.h>
#include "omega.h"

void omega_test(void)
{
  /* Create set S with inequalities:
   *    5x  -4y  -1 >= 0
   *   -9x  +8y     >= 0
   *    -x       +4 >= 0
   *     x          >= 0
   *    -y       +4 >= 0
   *     y          >= 0
   */

  Relation S(2);
  S.name_set_var(1, "x");
  S.name_set_var(2, "y");

  Variable_ID S_x = S.set_var(1);
  Variable_ID S_y = S.set_var(2);

  F_And *S_root = S.add_and();
  GEQ_Handle f1 = S_root->add_GEQ();
  f1.update_coef(S_x, 5);
  f1.update_coef(S_y, -4);
  f1.update_const(-1);

  GEQ_Handle f2 = S_root->add_GEQ();
  f2.update_coef(S_x, -9);
  f2.update_coef(S_y, 8);

  GEQ_Handle f3 = S_root->add_GEQ();
  f3.update_coef(S_x, -1);
  f3.update_const(4);

  GEQ_Handle f4 = S_root->add_GEQ();
  f4.update_coef(S_x, 1);

  GEQ_Handle f5 = S_root->add_GEQ();
  f5.update_coef(S_y, -1);
  f5.update_const(4);

  GEQ_Handle f6 = S_root->add_GEQ();
  f6.update_coef(S_y, 1);

  // Print the set that was built
  S.print();
  S.print_with_subs(); // FALSE after simplification

  // Is it satisfiable?
  if (S.is_upper_bound_satisfiable())
    printf("Omega test says satisfiable\n");
  else
    printf("Omega test says NOT satisfiable\n");
}

void enumerated_test(void)
{
  bool found = false;
  // Confirm satisfiability by enumerating points
  for (int y = 0; y <= 4; y++) {
    for (int x = 0; x <= 4; x++) {
      if ( 5 * x - 4 * y - 1 >= 0 &&
          -9 * x + 8 * y     >= 0)
        found = true;
    }
  }
  if (found)
    printf("Found a solution\n");
  else
    printf("No solution found\n");
}

int main(int argc, char **argv)
{
  enumerated_test();
  omega_test();
  return 0;
}