d9387208f072036e225e74b5147ed86281a9212f
[cvc5.git] / test / regress / regress0 / declare-fun-is-match.smt2
1 ; EXPECT: sat
2 (set-info :smt-lib-version 2.6)
3 (set-logic UFIDL)
4 (set-info :status sat)
5 (declare-fun match (Int Int) Int)
6 (declare-fun is (Int Int) Int)
7 (assert (= match is))
8 (check-sat)
9 (exit)