diff --git a/collects/redex/private/reduction-semantics.rkt b/collects/redex/private/reduction-semantics.rkt index aa16494ca5..cb10860145 100644 --- a/collects/redex/private/reduction-semantics.rkt +++ b/collects/redex/private/reduction-semantics.rkt @@ -259,12 +259,12 @@ #,rest-body)))) mtchs))] [(predicate) - #`(andmap (λ (mtch) - (let ([bindings (mtch-bindings mtch)]) - (let ([x (lookup-binding bindings 'names)] ...) - (term-let ([names/ellipses x] ...) - #,rest-body)))) - mtchs)] + #`(ormap (λ (mtch) + (let ([bindings (mtch-bindings mtch)]) + (let ([x (lookup-binding bindings 'names)] ...) + (term-let ([names/ellipses x] ...) + #,rest-body)))) + mtchs)] [else (error 'unknown-where-mode "~s" where-mode)]) #f))))))] [((-side-condition s ...) y ...) diff --git a/collects/redex/tests/rg-test.rkt b/collects/redex/tests/rg-test.rkt index 82321396c7..da279f97fa 100644 --- a/collects/redex/tests/rg-test.rkt +++ b/collects/redex/tests/rg-test.rkt @@ -862,6 +862,19 @@ (check-metafunction f (λ (_) #t))) 4) + (let () + (define-language L + ((m n) number)) + (define-metafunction L + [(f m_0 m_1 ...) + () + (where (n_0 ... n_i ...) (m_0 m_1 ...)) + (side-condition (null? (term (n_0 ...))))]) + (test + (with-handlers ([exn:fail:redex:generation-failure? (λ (_) #f)]) + (check-metafunction f (λ (_) #t) #:retries 1 #:print? #f #:attempts 1)) + #t)) + (test (output (λ () (check-metafunction m (λ (_) #t)))) #rx"no counterexamples") (test (output (λ () (check-metafunction m (curry eq? 1)))) #px"check-metafunction:.*counterexample found after 1 attempt with clause at .*:\\d+:\\d+")