I am trying to answer here but err:
forall(t in 0..4){
a[t]<=z[t];
-a[t]<=z[t];
x[t+1]==x[t]+v[t];
v[t+1]==v[t]+a[t];
}
I am trying to answer here but err:
forall(t in 0..4){
a[t]<=z[t];
-a[t]<=z[t];
x[t+1]==x[t]+v[t];
v[t+1]==v[t]+a[t];
}
The recursive equation enters into un-initialized interval hence index out of exeption. You can avoid this bug by tweaking: initialize not-needed valuations and assign them to zero.
This creates some overhead but simplifies the logic, cannot think about any simpler way to do this.