(assert (= x_0 1))
(assert (= x_1 1))