summaryrefslogtreecommitdiff
path: root/test/regress/regress0/parser/named-attr-error.smt2
blob: 2b925b8ce71a527f629d8f49d98b6120f7569e60 (plain) 
1
2
3
4
5
6

; REQUIRES: no-competition
; SCRUBBER: grep -o "Cannot name a term in a binder"
; EXPECT: Cannot name a term in a binder
; EXIT: 1
(set-logic QF_UF)
(define-fun f ((x Bool)) Bool (! x :named foo))
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback