The strange result of multiplication in formula

[Taeyang123456]

Hello! I am using dreal4 for some solving problem. However, when verifying the satisfiability of a formula containing multiplication, I encountered the following strange results. Here is a description of the problem after my actual problem has been reduced.

I wrote function sat_checker_main(), and replaced the original function in check_sat.cc dreal-cmake-example-project

void sat_checker_main() {
  const Variable x("x", Variable::Type::INTEGER);
  const Variable y("y", Variable::Type::INTEGER);
  const Formula f = (x <= 0) && (x > -2) && (y == 2 * x) && (y == -3);
  optional<Box> result = CheckSatisfiability(f, 0.001);
  if (result) {
    cout << f << " is delta-sat:\n" << *result << endl;
  } else {
    cout << f << " is unsat." << endl;
  }
}

When x is Integer, the formula generated by the above code should be unsat, but I got the output like this:

((y == -3) and (y == (2 * x)) and (x > -2) and (x <= 0)) is delta-sat:
x : [-1, -1]
y : [-3, -3]

It does not seem to satisfy the equation y==2*x. So I'm wondering if there is something wrong

[soonho-tri]

Thanks for the report! It's fixed by 08d2d6c. I'll release a new version soon.