Open pricsi opened 9 years ago
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.
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.