summaryrefslogtreecommitdiff
path: root/test/regress/regress0/bug541.smt2
blob: 771fbed4fb479f25e2cb8e2684c648d354502b68 (plain) 
1
2
3
4
5
6
7

; COMMAND-LINE: --lang=smt2.5
; 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