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

(set-logic QF_UF)
(declare-const x Bool)
(declare-const y Bool)
(define-fun f () Bool (! x :named foo))
(define-const g Bool (! y :named bar))
(assert (and foo bar))
(set-info :status sat)
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback