summaryrefslogtreecommitdiff
path: root/test/regress/regress0/bug541.smt2
blob: 482823985f987f230a02665fa155aa4ba35eec45 (plain)
1
2
3
4
5
6
; EXPECT: unsat
(set-logic ALL_SUPPORTED)
(declare-datatypes (T1 T2) ((Pair (mk-pair (first T1) (second T2)))))
(assert (= (mk-pair 0.0 0.0) (mk-pair 1.5 2.5)))
(check-sat)
(exit)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback