This repository was archived by the owner on May 11, 2021. It is now read-only.

Description
Given the following dReach specification:
[-1, 5] x;
[-1, 5] z;
[0, 10] time;
{ mode 1;
invt:
(z >= 0);
flow:
d/dt[x] = 1;
d/dt[z] = (2*x)-1;
jump:
}
init:
@1 (and (x = 0)(z = 0));
goal:
@1 (and (x >= 1.2));
The result is SAT but the expected result would be UNSAT as the invariant should prevent the system from progress.