;; Regression for #831. This used to saturate at `l(vec-of(k(b)))` because the
;; container child rebuilt in place and the query-side match was not revisited.
(sort E)
(sort VE (Vec E))
(constructor b () E)
(constructor k (E) E)
(constructor w (E) E)
(constructor l (VE) E)
(rewrite (w x) x)
(rewrite (l (vec-of (k x))) x)
(push)
(let $rebuilt (l (vec-of (w (k (b))))))
(run-schedule (saturate (run)))
(check (= $rebuilt (b)))
(pop)
(let $resolved (l (vec-of (k (b)))))
(run-schedule (saturate (run)))
(check (= $resolved (b)))