  This paper considers quasi-reductivity - essentially, the property that an
evaluation cannot get "stuck" due to a missing case in pattern matching - in
the context of term rewriting with logical constraints.
