summaryrefslogtreecommitdiff
path: root/test/regress/regress0/ho/qgu-fuzz-ho-1-dd.smt2
blob: 840db92a93fa4749407f95a2ac33e6984ff4e7b6 (plain) 
1
2
3
4
5
6

(set-logic HO_ALL)
(set-info :status sat)
(declare-const b (-> Int Int Int))
(declare-const c (-> Int Int))
(assert (and (= c (b 1)) (= c (b 0)) (> (b 1 0) 0) (> 0 (b 0 1)) (= 0 (c (b 0 0)))))
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback