projects
/
cvc5.git
/ blob
commit
grep
author
committer
pickaxe
?
search:
re
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)