summaryrefslogtreecommitdiff
path: root/test/regress/regress0/fmf/issue4260-arrays-card-one.smt2
blob: bdd5e33476075ed4bbd309c8e1bbbc1806c39a7b (plain) 
1
2
3
4
5
6
7
8

; COMMAND-LINE: --finite-model-find
; EXPECT: sat
(set-logic AUFNIA)
(declare-sort S0 0)
(declare-const a (Array Int S0))
(declare-const b (Array Int S0))
(assert (distinct b a))
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback