more tests. subst can make a failing program pass, because subst doesn't check that the assignment satisfies the constraints, and substitutes in, blowing away the constraints regardless