Problem with higher order functions when using invariants #97

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.