path: root/test/regress/regress2/strings/strings-alpha-card-129.smt2

; COMMAND-LINE: --strings-alpha-card=128 --simplification=none
; EXPECT: unsat
(set-logic QF_SLIA)
(declare-fun s1 () String)
(assert (= (str.len s1) 1))
(declare-fun s2 () String)
(assert (= (str.len s2) 1))
(declare-fun s3 () String)
(assert (= (str.len s3) 1))
(declare-fun s4 () String)
(assert (= (str.len s4) 1))
(declare-fun s5 () String)
(assert (= (str.len s5) 1))
(declare-fun s6 () String)
(assert (= (str.len s6) 1))
(declare-fun s7 () String)
(assert (= (str.len s7) 1))
(declare-fun s8 () String)
(assert (= (str.len s8) 1))
(declare-fun s9 () String)
(assert (= (str.len s9) 1))
(declare-fun s10 () String)
(assert (= (str.len s10) 1))
(declare-fun s11 () String)
(assert (= (str.len s11) 1))
(declare-fun s12 () String)
(assert (= (str.len s12) 1))
(declare-fun s13 () String)
(assert (= (str.len s13) 1))
(declare-fun s14 () String)
(assert (= (str.len s14) 1))
(declare-fun s15 () String)
(assert (= (str.len s15) 1))
(declare-fun s16 () String)
(assert (= (str.len s16) 1))
(declare-fun s17 () String)
(assert (= (str.len s17) 1))
(declare-fun s18 () String)
(assert (= (str.len s18) 1))
(declare-fun s19 () String)
(assert (= (str.len s19) 1))
(declare-fun s20 () String)
(assert (= (str.len s20) 1))
(declare-fun s21 () String)
(assert (= (str.len s21) 1))
(declare-fun s22 () String)
(assert (= (str.len s22) 1))
(declare-fun s23 () String)
(assert (= (str.len s23) 1))
(declare-fun s24 () String)
(assert (= (str.len s24) 1))
(declare-fun s25 () String)
(assert (= (str.len s25) 1))
(declare-fun s26 () String)
(assert (= (str.len s26) 1))
(declare-fun s27 () String)
(assert (= (str.len s27) 1))
(declare-fun s28 () String)
(assert (= (str.len s28) 1))
(declare-fun s29 () String)
(assert (= (str.len s29) 1))
(declare-fun s30 () String)
(assert (= (str.len s30) 1))
(declare-fun s31 () String)
(assert (= (str.len s31) 1))
(declare-fun s32 () String)
(assert (= (str.len s32) 1))
(declare-fun s33 () String)
(assert (= (str.len s33) 1))
(declare-fun s34 () String)
(assert (= (str.len s34) 1))
(declare-fun s35 () String)
(assert (= (str.len s35) 1))
(declare-fun s36 () String)
(assert (= (str.len s36) 1))
(declare-fun s37 () String)
(assert (= (str.len s37) 1))
(declare-fun s38 () String)
(assert (= (str.len s38) 1))
(declare-fun s39 () String)
(assert (= (str.len s39) 1))
(declare-fun s40 () String)
(assert (= (str.len s40) 1))
(declare-fun s41 () String)
(assert (= (str.len s41) 1))
(declare-fun s42 () String)
(assert (= (str.len s42) 1))
(declare-fun s43 () String)
(assert (= (str.len s43) 1))
(declare-fun s44 () String)
(assert (= (str.len s44) 1))
(declare-fun s45 () String)
(assert (= (str.len s45) 1))
(declare-fun s46 () String)
(assert (= (str.len s46) 1))
(declare-fun s47 () String)
(assert (= (str.len s47) 1))
(declare-fun s48 () String)
(assert (= (str.len s48) 1))
(declare-fun s49 () String)
(assert (= (str.len s49) 1))
(declare-fun s50 () String)
(assert (= (str.len s50) 1))
(declare-fun s51 () String)
(assert (= (str.len s51) 1))
(declare-fun s52 () String)
(assert (= (str.len s52) 1))
(declare-fun s53 () String)
(assert (= (str.len s53) 1))
(declare-fun s54 () String)
(assert (= (str.len s54) 1))
(declare-fun s55 () String)
(assert (= (str.len s55) 1))
(declare-fun s56 () String)
(assert (= (str.len s56) 1))
(declare-fun s57 () String)
(assert (= (str.len s57) 1))
(declare-fun s58 () String)
(assert (= (str.len s58) 1))
(declare-fun s59 () String)
(assert (= (str.len s59) 1))
(declare-fun s60 () String)
(assert (= (str.len s60) 1))
(declare-fun s61 () String)
(assert (= (str.len s61) 1))
(declare-fun s62 () String)
(assert (= (str.len s62) 1))
(declare-fun s63 () String)
(assert (= (str.len s63) 1))
(declare-fun s64 () String)
(assert (= (str.len s64) 1))
(declare-fun s65 () String)
(assert (= (str.len s65) 1))
(declare-fun s66 () String)
(assert (= (str.len s66) 1))
(declare-fun s67 () String)
(assert (= (str.len s67) 1))
(declare-fun s68 () String)
(assert (= (str.len s68) 1))
(declare-fun s69 () String)
(assert (= (str.len s69) 1))
(declare-fun s70 () String)
(assert (= (str.len s70) 1))
(declare-fun s71 () String)
(assert (= (str.len s71) 1))
(declare-fun s72 () String)
(assert (= (str.len s72) 1))
(declare-fun s73 () String)
(assert (= (str.len s73) 1))
(declare-fun s74 () String)
(assert (= (str.len s74) 1))
(declare-fun s75 () String)
(assert (= (str.len s75) 1))
(declare-fun s76 () String)
(assert (= (str.len s76) 1))
(declare-fun s77 () String)
(assert (= (str.len s77) 1))
(declare-fun s78 () String)
(assert (= (str.len s78) 1))
(declare-fun s79 () String)
(assert (= (str.len s79) 1))
(declare-fun s80 () String)
(assert (= (str.len s80) 1))
(declare-fun s81 () String)
(assert (= (str.len s81) 1))
(declare-fun s82 () String)
(assert (= (str.len s82) 1))
(declare-fun s83 () String)
(assert (= (str.len s83) 1))
(declare-fun s84 () String)
(assert (= (str.len s84) 1))
(declare-fun s85 () String)
(assert (= (str.len s85) 1))
(declare-fun s86 () String)
(assert (= (str.len s86) 1))
(declare-fun s87 () String)
(assert (= (str.len s87) 1))
(declare-fun s88 () String)
(assert (= (str.len s88) 1))
(declare-fun s89 () String)
(assert (= (str.len s89) 1))
(declare-fun s90 () String)
(assert (= (str.len s90) 1))
(declare-fun s91 () String)
(assert (= (str.len s91) 1))
(declare-fun s92 () String)
(assert (= (str.len s92) 1))
(declare-fun s93 () String)
(assert (= (str.len s93) 1))
(declare-fun s94 () String)
(assert (= (str.len s94) 1))
(declare-fun s95 () String)
(assert (= (str.len s95) 1))
(declare-fun s96 () String)
(assert (= (str.len s96) 1))
(declare-fun s97 () String)
(assert (= (str.len s97) 1))
(declare-fun s98 () String)
(assert (= (str.len s98) 1))
(declare-fun s99 () String)
(assert (= (str.len s99) 1))
(declare-fun s100 () String)
(assert (= (str.len s100) 1))
(declare-fun s101 () String)
(assert (= (str.len s101) 1))
(declare-fun s102 () String)
(assert (= (str.len s102) 1))
(declare-fun s103 () String)
(assert (= (str.len s103) 1))
(declare-fun s104 () String)
(assert (= (str.len s104) 1))
(declare-fun s105 () String)
(assert (= (str.len s105) 1))
(declare-fun s106 () String)
(assert (= (str.len s106) 1))
(declare-fun s107 () String)
(assert (= (str.len s107) 1))
(declare-fun s108 () String)
(assert (= (str.len s108) 1))
(declare-fun s109 () String)
(assert (= (str.len s109) 1))
(declare-fun s110 () String)
(assert (= (str.len s110) 1))
(declare-fun s111 () String)
(assert (= (str.len s111) 1))
(declare-fun s112 () String)
(assert (= (str.len s112) 1))
(declare-fun s113 () String)
(assert (= (str.len s113) 1))
(declare-fun s114 () String)
(assert (= (str.len s114) 1))
(declare-fun s115 () String)
(assert (= (str.len s115) 1))
(declare-fun s116 () String)
(assert (= (str.len s116) 1))
(declare-fun s117 () String)
(assert (= (str.len s117) 1))
(declare-fun s118 () String)
(assert (= (str.len s118) 1))
(declare-fun s119 () String)
(assert (= (str.len s119) 1))
(declare-fun s120 () String)
(assert (= (str.len s120) 1))
(declare-fun s121 () String)
(assert (= (str.len s121) 1))
(declare-fun s122 () String)
(assert (= (str.len s122) 1))
(declare-fun s123 () String)
(assert (= (str.len s123) 1))
(declare-fun s124 () String)
(assert (= (str.len s124) 1))
(declare-fun s125 () String)
(assert (= (str.len s125) 1))
(declare-fun s126 () String)
(assert (= (str.len s126) 1))
(declare-fun s127 () String)
(assert (= (str.len s127) 1))
(declare-fun s128 () String)
(assert (= (str.len s128) 1))
(declare-fun s129 () String)
(assert (= (str.len s129) 1))
(assert (distinct
s1
s2
s3
s4
s5
s6
s7
s8
s9
s10
s11
s12
s13
s14
s15
s16
s17
s18
s19
s20
s21
s22
s23
s24
s25
s26
s27
s28
s29
s30
s31
s32
s33
s34
s35
s36
s37
s38
s39
s40
s41
s42
s43
s44
s45
s46
s47
s48
s49
s50
s51
s52
s53
s54
s55
s56
s57
s58
s59
s60
s61
s62
s63
s64
s65
s66
s67
s68
s69
s70
s71
s72
s73
s74
s75
s76
s77
s78
s79
s80
s81
s82
s83
s84
s85
s86
s87
s88
s89
s90
s91
s92
s93
s94
s95
s96
s97
s98
s99
s100
s101
s102
s103
s104
s105
s106
s107
s108
s109
s110
s111
s112
s113
s114
s115
s116
s117
s118
s119
s120
s121
s122
s123
s124
s125
s126
s127
s128
s129
))
(check-sat)