summaryrefslogtreecommitdiff
path: root/test/regress/regress0/quantifiers/simp-typ-test.smt2
blob: 380a66aac17c20e3a5c4e14b755f5bc80d508039 (plain) 
1
2
3
4
5
6
7

(set-logic UFLIRA)
(set-info :status unsat)
; ensure that E-matching matches on sub-types
(declare-fun P (Real) Bool)
(assert (forall ((x Real)) (P x)))
(assert (not (P 5)))
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback