[ Eq(x3, 1*floor(t/k5)) ]