** Calling: z3 -nw -in -smt2
[GOOD] ; Automatically generated by SBV. Do not edit.
[GOOD] (set-option :print-success true)
[GOOD] (set-option :global-declarations true)
[GOOD] (set-option :smtlib2_compliant true)
[GOOD] (set-option :diagnostic-output-channel "stdout")
[GOOD] (set-option :produce-models true)
[GOOD] (set-logic ALL)
[GOOD] ; --- uninterpreted sorts ---
[GOOD] ; --- literal constants ---
[GOOD] (define-fun s_2 () Bool false)
[GOOD] (define-fun s_1 () Bool true)
[GOOD] (define-fun s2 () Int 1)
[GOOD] ; --- skolem constants ---
[GOOD] (declare-fun s0 () String) ; tracks user variable "s"
[GOOD] ; --- constant tables ---
[GOOD] ; --- skolemized tables ---
[GOOD] ; --- arrays ---
[GOOD] ; --- uninterpreted constants ---
[GOOD] ; --- user given axioms ---
[GOOD] ; --- formula ---
[GOOD] (define-fun s1 () Int (str.len s0))
[GOOD] (define-fun s3 () Bool (= s1 s2))
[GOOD] (assert s3)
*** Checking Satisfiability, all solutions..
Looking for solution 1
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\x00"))
[GOOD] (define-fun s4 () String "\x00")
[GOOD] (define-fun s5 () Bool (distinct s0 s4))
[GOOD] (assert s5)
Looking for solution 2
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 " "))
[GOOD] (define-fun s6 () String " ")
[GOOD] (define-fun s7 () Bool (distinct s0 s6))
[GOOD] (assert s7)
Looking for solution 3
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\x01"))
[GOOD] (define-fun s8 () String "\x01")
[GOOD] (define-fun s9 () Bool (distinct s0 s8))
[GOOD] (assert s9)
Looking for solution 4
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "!"))
[GOOD] (define-fun s10 () String "!")
[GOOD] (define-fun s11 () Bool (distinct s0 s10))
[GOOD] (assert s11)
Looking for solution 5
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\x10"))
[GOOD] (define-fun s12 () String "\x10")
[GOOD] (define-fun s13 () Bool (distinct s0 s12))
[GOOD] (assert s13)
Looking for solution 6
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "0"))
[GOOD] (define-fun s14 () String "0")
[GOOD] (define-fun s15 () Bool (distinct s0 s14))
[GOOD] (assert s15)
Looking for solution 7
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\x11"))
[GOOD] (define-fun s16 () String "\x11")
[GOOD] (define-fun s17 () Bool (distinct s0 s16))
[GOOD] (assert s17)
Looking for solution 8
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "1"))
[GOOD] (define-fun s18 () String "1")
[GOOD] (define-fun s19 () Bool (distinct s0 s18))
[GOOD] (assert s19)
Looking for solution 9
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\x08"))
[GOOD] (define-fun s20 () String "\x08")
[GOOD] (define-fun s21 () Bool (distinct s0 s20))
[GOOD] (assert s21)
Looking for solution 10
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "("))
[GOOD] (define-fun s22 () String "(")
[GOOD] (define-fun s23 () Bool (distinct s0 s22))
[GOOD] (assert s23)
Looking for solution 11
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\x09"))
[GOOD] (define-fun s24 () String "\x09")
[GOOD] (define-fun s25 () Bool (distinct s0 s24))
[GOOD] (assert s25)
Looking for solution 12
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 ")"))
[GOOD] (define-fun s26 () String ")")
[GOOD] (define-fun s27 () Bool (distinct s0 s26))
[GOOD] (assert s27)
Looking for solution 13
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\x18"))
[GOOD] (define-fun s28 () String "\x18")
[GOOD] (define-fun s29 () Bool (distinct s0 s28))
[GOOD] (assert s29)
Looking for solution 14
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "8"))
[GOOD] (define-fun s30 () String "8")
[GOOD] (define-fun s31 () Bool (distinct s0 s30))
[GOOD] (assert s31)
Looking for solution 15
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\x19"))
[GOOD] (define-fun s32 () String "\x19")
[GOOD] (define-fun s33 () Bool (distinct s0 s32))
[GOOD] (assert s33)
Looking for solution 16
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "9"))
[GOOD] (define-fun s34 () String "9")
[GOOD] (define-fun s35 () Bool (distinct s0 s34))
[GOOD] (assert s35)
Looking for solution 17
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\x02"))
[GOOD] (define-fun s36 () String "\x02")
[GOOD] (define-fun s37 () Bool (distinct s0 s36))
[GOOD] (assert s37)
Looking for solution 18
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 """"))
[GOOD] (define-fun s38 () String """")
[GOOD] (define-fun s39 () Bool (distinct s0 s38))
[GOOD] (assert s39)
Looking for solution 19
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\x03"))
[GOOD] (define-fun s40 () String "\x03")
[GOOD] (define-fun s41 () Bool (distinct s0 s40))
[GOOD] (assert s41)
Looking for solution 20
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "#"))
[GOOD] (define-fun s42 () String "#")
[GOOD] (define-fun s43 () Bool (distinct s0 s42))
[GOOD] (assert s43)
Looking for solution 21
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\x12"))
[GOOD] (define-fun s44 () String "\x12")
[GOOD] (define-fun s45 () Bool (distinct s0 s44))
[GOOD] (assert s45)
Looking for solution 22
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "2"))
[GOOD] (define-fun s46 () String "2")
[GOOD] (define-fun s47 () Bool (distinct s0 s46))
[GOOD] (assert s47)
Looking for solution 23
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\x13"))
[GOOD] (define-fun s48 () String "\x13")
[GOOD] (define-fun s49 () Bool (distinct s0 s48))
[GOOD] (assert s49)
Looking for solution 24
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "3"))
[GOOD] (define-fun s50 () String "3")
[GOOD] (define-fun s51 () Bool (distinct s0 s50))
[GOOD] (assert s51)
Looking for solution 25
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\n"))
[GOOD] (define-fun s52 () String "\n")
[GOOD] (define-fun s53 () Bool (distinct s0 s52))
[GOOD] (assert s53)
Looking for solution 26
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "*"))
[GOOD] (define-fun s54 () String "*")
[GOOD] (define-fun s55 () Bool (distinct s0 s54))
[GOOD] (assert s55)
Looking for solution 27
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\v"))
[GOOD] (define-fun s56 () String "\v")
[GOOD] (define-fun s57 () Bool (distinct s0 s56))
[GOOD] (assert s57)
Looking for solution 28
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "+"))
[GOOD] (define-fun s58 () String "+")
[GOOD] (define-fun s59 () Bool (distinct s0 s58))
[GOOD] (assert s59)
Looking for solution 29
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\x1A"))
[GOOD] (define-fun s60 () String "\x1A")
[GOOD] (define-fun s61 () Bool (distinct s0 s60))
[GOOD] (assert s61)
Looking for solution 30
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 ":"))
[GOOD] (define-fun s62 () String ":")
[GOOD] (define-fun s63 () Bool (distinct s0 s62))
[GOOD] (assert s63)
Looking for solution 31
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\x1B"))
[GOOD] (define-fun s64 () String "\x1B")
[GOOD] (define-fun s65 () Bool (distinct s0 s64))
[GOOD] (assert s65)
Looking for solution 32
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 ";"))
[GOOD] (define-fun s66 () String ";")
[GOOD] (define-fun s67 () Bool (distinct s0 s66))
[GOOD] (assert s67)
Looking for solution 33
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\x04"))
[GOOD] (define-fun s68 () String "\x04")
[GOOD] (define-fun s69 () Bool (distinct s0 s68))
[GOOD] (assert s69)
Looking for solution 34
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "$"))
[GOOD] (define-fun s70 () String "$")
[GOOD] (define-fun s71 () Bool (distinct s0 s70))
[GOOD] (assert s71)
Looking for solution 35
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\x05"))
[GOOD] (define-fun s72 () String "\x05")
[GOOD] (define-fun s73 () Bool (distinct s0 s72))
[GOOD] (assert s73)
Looking for solution 36
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "%"))
[GOOD] (define-fun s74 () String "%")
[GOOD] (define-fun s75 () Bool (distinct s0 s74))
[GOOD] (assert s75)
Looking for solution 37
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\x14"))
[GOOD] (define-fun s76 () String "\x14")
[GOOD] (define-fun s77 () Bool (distinct s0 s76))
[GOOD] (assert s77)
Looking for solution 38
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "4"))
[GOOD] (define-fun s78 () String "4")
[GOOD] (define-fun s79 () Bool (distinct s0 s78))
[GOOD] (assert s79)
Looking for solution 39
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\x15"))
[GOOD] (define-fun s80 () String "\x15")
[GOOD] (define-fun s81 () Bool (distinct s0 s80))
[GOOD] (assert s81)
Looking for solution 40
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "5"))
[GOOD] (define-fun s82 () String "5")
[GOOD] (define-fun s83 () Bool (distinct s0 s82))
[GOOD] (assert s83)
Looking for solution 41
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\f"))
[GOOD] (define-fun s84 () String "\f")
[GOOD] (define-fun s85 () Bool (distinct s0 s84))
[GOOD] (assert s85)
Looking for solution 42
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 ","))
[GOOD] (define-fun s86 () String ",")
[GOOD] (define-fun s87 () Bool (distinct s0 s86))
[GOOD] (assert s87)
Looking for solution 43
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\r"))
[GOOD] (define-fun s88 () String "\r")
[GOOD] (define-fun s89 () Bool (distinct s0 s88))
[GOOD] (assert s89)
Looking for solution 44
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "-"))
[GOOD] (define-fun s90 () String "-")
[GOOD] (define-fun s91 () Bool (distinct s0 s90))
[GOOD] (assert s91)
Looking for solution 45
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\x1C"))
[GOOD] (define-fun s92 () String "\x1C")
[GOOD] (define-fun s93 () Bool (distinct s0 s92))
[GOOD] (assert s93)
Looking for solution 46
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "<"))
[GOOD] (define-fun s94 () String "<")
[GOOD] (define-fun s95 () Bool (distinct s0 s94))
[GOOD] (assert s95)
Looking for solution 47
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\x1D"))
[GOOD] (define-fun s96 () String "\x1D")
[GOOD] (define-fun s97 () Bool (distinct s0 s96))
[GOOD] (assert s97)
Looking for solution 48
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "="))
[GOOD] (define-fun s98 () String "=")
[GOOD] (define-fun s99 () Bool (distinct s0 s98))
[GOOD] (assert s99)
Looking for solution 49
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\x06"))
[GOOD] (define-fun s100 () String "\x06")
[GOOD] (define-fun s101 () Bool (distinct s0 s100))
[GOOD] (assert s101)
Looking for solution 50
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "&"))
[GOOD] (define-fun s102 () String "&")
[GOOD] (define-fun s103 () Bool (distinct s0 s102))
[GOOD] (assert s103)
Looking for solution 51
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\x07"))
[GOOD] (define-fun s104 () String "\x07")
[GOOD] (define-fun s105 () Bool (distinct s0 s104))
[GOOD] (assert s105)
Looking for solution 52
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "'"))
[GOOD] (define-fun s106 () String "'")
[GOOD] (define-fun s107 () Bool (distinct s0 s106))
[GOOD] (assert s107)
Looking for solution 53
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\x16"))
[GOOD] (define-fun s108 () String "\x16")
[GOOD] (define-fun s109 () Bool (distinct s0 s108))
[GOOD] (assert s109)
Looking for solution 54
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "6"))
[GOOD] (define-fun s110 () String "6")
[GOOD] (define-fun s111 () Bool (distinct s0 s110))
[GOOD] (assert s111)
Looking for solution 55
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\x17"))
[GOOD] (define-fun s112 () String "\x17")
[GOOD] (define-fun s113 () Bool (distinct s0 s112))
[GOOD] (assert s113)
Looking for solution 56
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "7"))
[GOOD] (define-fun s114 () String "7")
[GOOD] (define-fun s115 () Bool (distinct s0 s114))
[GOOD] (assert s115)
Looking for solution 57
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\x0E"))
[GOOD] (define-fun s116 () String "\x0E")
[GOOD] (define-fun s117 () Bool (distinct s0 s116))
[GOOD] (assert s117)
Looking for solution 58
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "."))
[GOOD] (define-fun s118 () String ".")
[GOOD] (define-fun s119 () Bool (distinct s0 s118))
[GOOD] (assert s119)
Looking for solution 59
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\x0F"))
[GOOD] (define-fun s120 () String "\x0F")
[GOOD] (define-fun s121 () Bool (distinct s0 s120))
[GOOD] (assert s121)
Looking for solution 60
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "/"))
[GOOD] (define-fun s122 () String "/")
[GOOD] (define-fun s123 () Bool (distinct s0 s122))
[GOOD] (assert s123)
Looking for solution 61
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\x1E"))
[GOOD] (define-fun s124 () String "\x1E")
[GOOD] (define-fun s125 () Bool (distinct s0 s124))
[GOOD] (assert s125)
Looking for solution 62
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 ">"))
[GOOD] (define-fun s126 () String ">")
[GOOD] (define-fun s127 () Bool (distinct s0 s126))
[GOOD] (assert s127)
Looking for solution 63
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\x1F"))
[GOOD] (define-fun s128 () String "\x1F")
[GOOD] (define-fun s129 () Bool (distinct s0 s128))
[GOOD] (assert s129)
Looking for solution 64
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "?"))
[GOOD] (define-fun s130 () String "?")
[GOOD] (define-fun s131 () Bool (distinct s0 s130))
[GOOD] (assert s131)
Looking for solution 65
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\x80"))
[GOOD] (define-fun s132 () String "\x80")
[GOOD] (define-fun s133 () Bool (distinct s0 s132))
[GOOD] (assert s133)
Looking for solution 66
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xa0"))
[GOOD] (define-fun s134 () String "\xa0")
[GOOD] (define-fun s135 () Bool (distinct s0 s134))
[GOOD] (assert s135)
Looking for solution 67
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\x81"))
[GOOD] (define-fun s136 () String "\x81")
[GOOD] (define-fun s137 () Bool (distinct s0 s136))
[GOOD] (assert s137)
Looking for solution 68
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xa1"))
[GOOD] (define-fun s138 () String "\xa1")
[GOOD] (define-fun s139 () Bool (distinct s0 s138))
[GOOD] (assert s139)
Looking for solution 69
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\x90"))
[GOOD] (define-fun s140 () String "\x90")
[GOOD] (define-fun s141 () Bool (distinct s0 s140))
[GOOD] (assert s141)
Looking for solution 70
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xb0"))
[GOOD] (define-fun s142 () String "\xb0")
[GOOD] (define-fun s143 () Bool (distinct s0 s142))
[GOOD] (assert s143)
Looking for solution 71
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\x91"))
[GOOD] (define-fun s144 () String "\x91")
[GOOD] (define-fun s145 () Bool (distinct s0 s144))
[GOOD] (assert s145)
Looking for solution 72
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xb1"))
[GOOD] (define-fun s146 () String "\xb1")
[GOOD] (define-fun s147 () Bool (distinct s0 s146))
[GOOD] (assert s147)
Looking for solution 73
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\x88"))
[GOOD] (define-fun s148 () String "\x88")
[GOOD] (define-fun s149 () Bool (distinct s0 s148))
[GOOD] (assert s149)
Looking for solution 74
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xa8"))
[GOOD] (define-fun s150 () String "\xa8")
[GOOD] (define-fun s151 () Bool (distinct s0 s150))
[GOOD] (assert s151)
Looking for solution 75
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\x89"))
[GOOD] (define-fun s152 () String "\x89")
[GOOD] (define-fun s153 () Bool (distinct s0 s152))
[GOOD] (assert s153)
Looking for solution 76
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xa9"))
[GOOD] (define-fun s154 () String "\xa9")
[GOOD] (define-fun s155 () Bool (distinct s0 s154))
[GOOD] (assert s155)
Looking for solution 77
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\x98"))
[GOOD] (define-fun s156 () String "\x98")
[GOOD] (define-fun s157 () Bool (distinct s0 s156))
[GOOD] (assert s157)
Looking for solution 78
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xb8"))
[GOOD] (define-fun s158 () String "\xb8")
[GOOD] (define-fun s159 () Bool (distinct s0 s158))
[GOOD] (assert s159)
Looking for solution 79
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\x99"))
[GOOD] (define-fun s160 () String "\x99")
[GOOD] (define-fun s161 () Bool (distinct s0 s160))
[GOOD] (assert s161)
Looking for solution 80
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xb9"))
[GOOD] (define-fun s162 () String "\xb9")
[GOOD] (define-fun s163 () Bool (distinct s0 s162))
[GOOD] (assert s163)
Looking for solution 81
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\x82"))
[GOOD] (define-fun s164 () String "\x82")
[GOOD] (define-fun s165 () Bool (distinct s0 s164))
[GOOD] (assert s165)
Looking for solution 82
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xa2"))
[GOOD] (define-fun s166 () String "\xa2")
[GOOD] (define-fun s167 () Bool (distinct s0 s166))
[GOOD] (assert s167)
Looking for solution 83
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\x83"))
[GOOD] (define-fun s168 () String "\x83")
[GOOD] (define-fun s169 () Bool (distinct s0 s168))
[GOOD] (assert s169)
Looking for solution 84
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xa3"))
[GOOD] (define-fun s170 () String "\xa3")
[GOOD] (define-fun s171 () Bool (distinct s0 s170))
[GOOD] (assert s171)
Looking for solution 85
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\x92"))
[GOOD] (define-fun s172 () String "\x92")
[GOOD] (define-fun s173 () Bool (distinct s0 s172))
[GOOD] (assert s173)
Looking for solution 86
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xb2"))
[GOOD] (define-fun s174 () String "\xb2")
[GOOD] (define-fun s175 () Bool (distinct s0 s174))
[GOOD] (assert s175)
Looking for solution 87
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\x93"))
[GOOD] (define-fun s176 () String "\x93")
[GOOD] (define-fun s177 () Bool (distinct s0 s176))
[GOOD] (assert s177)
Looking for solution 88
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xb3"))
[GOOD] (define-fun s178 () String "\xb3")
[GOOD] (define-fun s179 () Bool (distinct s0 s178))
[GOOD] (assert s179)
Looking for solution 89
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\x8a"))
[GOOD] (define-fun s180 () String "\x8a")
[GOOD] (define-fun s181 () Bool (distinct s0 s180))
[GOOD] (assert s181)
Looking for solution 90
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xaa"))
[GOOD] (define-fun s182 () String "\xaa")
[GOOD] (define-fun s183 () Bool (distinct s0 s182))
[GOOD] (assert s183)
Looking for solution 91
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\x8b"))
[GOOD] (define-fun s184 () String "\x8b")
[GOOD] (define-fun s185 () Bool (distinct s0 s184))
[GOOD] (assert s185)
Looking for solution 92
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xab"))
[GOOD] (define-fun s186 () String "\xab")
[GOOD] (define-fun s187 () Bool (distinct s0 s186))
[GOOD] (assert s187)
Looking for solution 93
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\x9a"))
[GOOD] (define-fun s188 () String "\x9a")
[GOOD] (define-fun s189 () Bool (distinct s0 s188))
[GOOD] (assert s189)
Looking for solution 94
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xba"))
[GOOD] (define-fun s190 () String "\xba")
[GOOD] (define-fun s191 () Bool (distinct s0 s190))
[GOOD] (assert s191)
Looking for solution 95
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\x9b"))
[GOOD] (define-fun s192 () String "\x9b")
[GOOD] (define-fun s193 () Bool (distinct s0 s192))
[GOOD] (assert s193)
Looking for solution 96
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xbb"))
[GOOD] (define-fun s194 () String "\xbb")
[GOOD] (define-fun s195 () Bool (distinct s0 s194))
[GOOD] (assert s195)
Looking for solution 97
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\x84"))
[GOOD] (define-fun s196 () String "\x84")
[GOOD] (define-fun s197 () Bool (distinct s0 s196))
[GOOD] (assert s197)
Looking for solution 98
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xa4"))
[GOOD] (define-fun s198 () String "\xa4")
[GOOD] (define-fun s199 () Bool (distinct s0 s198))
[GOOD] (assert s199)
Looking for solution 99
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\x85"))
[GOOD] (define-fun s200 () String "\x85")
[GOOD] (define-fun s201 () Bool (distinct s0 s200))
[GOOD] (assert s201)
Looking for solution 100
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xa5"))
[GOOD] (define-fun s202 () String "\xa5")
[GOOD] (define-fun s203 () Bool (distinct s0 s202))
[GOOD] (assert s203)
Looking for solution 101
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\x94"))
[GOOD] (define-fun s204 () String "\x94")
[GOOD] (define-fun s205 () Bool (distinct s0 s204))
[GOOD] (assert s205)
Looking for solution 102
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xb4"))
[GOOD] (define-fun s206 () String "\xb4")
[GOOD] (define-fun s207 () Bool (distinct s0 s206))
[GOOD] (assert s207)
Looking for solution 103
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\x95"))
[GOOD] (define-fun s208 () String "\x95")
[GOOD] (define-fun s209 () Bool (distinct s0 s208))
[GOOD] (assert s209)
Looking for solution 104
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xb5"))
[GOOD] (define-fun s210 () String "\xb5")
[GOOD] (define-fun s211 () Bool (distinct s0 s210))
[GOOD] (assert s211)
Looking for solution 105
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\x8c"))
[GOOD] (define-fun s212 () String "\x8c")
[GOOD] (define-fun s213 () Bool (distinct s0 s212))
[GOOD] (assert s213)
Looking for solution 106
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xac"))
[GOOD] (define-fun s214 () String "\xac")
[GOOD] (define-fun s215 () Bool (distinct s0 s214))
[GOOD] (assert s215)
Looking for solution 107
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\x8d"))
[GOOD] (define-fun s216 () String "\x8d")
[GOOD] (define-fun s217 () Bool (distinct s0 s216))
[GOOD] (assert s217)
Looking for solution 108
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xad"))
[GOOD] (define-fun s218 () String "\xad")
[GOOD] (define-fun s219 () Bool (distinct s0 s218))
[GOOD] (assert s219)
Looking for solution 109
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\x9c"))
[GOOD] (define-fun s220 () String "\x9c")
[GOOD] (define-fun s221 () Bool (distinct s0 s220))
[GOOD] (assert s221)
Looking for solution 110
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xbc"))
[GOOD] (define-fun s222 () String "\xbc")
[GOOD] (define-fun s223 () Bool (distinct s0 s222))
[GOOD] (assert s223)
Looking for solution 111
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\x9d"))
[GOOD] (define-fun s224 () String "\x9d")
[GOOD] (define-fun s225 () Bool (distinct s0 s224))
[GOOD] (assert s225)
Looking for solution 112
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xbd"))
[GOOD] (define-fun s226 () String "\xbd")
[GOOD] (define-fun s227 () Bool (distinct s0 s226))
[GOOD] (assert s227)
Looking for solution 113
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\x86"))
[GOOD] (define-fun s228 () String "\x86")
[GOOD] (define-fun s229 () Bool (distinct s0 s228))
[GOOD] (assert s229)
Looking for solution 114
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xa6"))
[GOOD] (define-fun s230 () String "\xa6")
[GOOD] (define-fun s231 () Bool (distinct s0 s230))
[GOOD] (assert s231)
Looking for solution 115
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\x87"))
[GOOD] (define-fun s232 () String "\x87")
[GOOD] (define-fun s233 () Bool (distinct s0 s232))
[GOOD] (assert s233)
Looking for solution 116
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xa7"))
[GOOD] (define-fun s234 () String "\xa7")
[GOOD] (define-fun s235 () Bool (distinct s0 s234))
[GOOD] (assert s235)
Looking for solution 117
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\x96"))
[GOOD] (define-fun s236 () String "\x96")
[GOOD] (define-fun s237 () Bool (distinct s0 s236))
[GOOD] (assert s237)
Looking for solution 118
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xb6"))
[GOOD] (define-fun s238 () String "\xb6")
[GOOD] (define-fun s239 () Bool (distinct s0 s238))
[GOOD] (assert s239)
Looking for solution 119
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\x97"))
[GOOD] (define-fun s240 () String "\x97")
[GOOD] (define-fun s241 () Bool (distinct s0 s240))
[GOOD] (assert s241)
Looking for solution 120
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xb7"))
[GOOD] (define-fun s242 () String "\xb7")
[GOOD] (define-fun s243 () Bool (distinct s0 s242))
[GOOD] (assert s243)
Looking for solution 121
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\x8e"))
[GOOD] (define-fun s244 () String "\x8e")
[GOOD] (define-fun s245 () Bool (distinct s0 s244))
[GOOD] (assert s245)
Looking for solution 122
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xae"))
[GOOD] (define-fun s246 () String "\xae")
[GOOD] (define-fun s247 () Bool (distinct s0 s246))
[GOOD] (assert s247)
Looking for solution 123
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\x8f"))
[GOOD] (define-fun s248 () String "\x8f")
[GOOD] (define-fun s249 () Bool (distinct s0 s248))
[GOOD] (assert s249)
Looking for solution 124
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xaf"))
[GOOD] (define-fun s250 () String "\xaf")
[GOOD] (define-fun s251 () Bool (distinct s0 s250))
[GOOD] (assert s251)
Looking for solution 125
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\x9e"))
[GOOD] (define-fun s252 () String "\x9e")
[GOOD] (define-fun s253 () Bool (distinct s0 s252))
[GOOD] (assert s253)
Looking for solution 126
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xbe"))
[GOOD] (define-fun s254 () String "\xbe")
[GOOD] (define-fun s255 () Bool (distinct s0 s254))
[GOOD] (assert s255)
Looking for solution 127
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\x9f"))
[GOOD] (define-fun s256 () String "\x9f")
[GOOD] (define-fun s257 () Bool (distinct s0 s256))
[GOOD] (assert s257)
Looking for solution 128
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xbf"))
[GOOD] (define-fun s258 () String "\xbf")
[GOOD] (define-fun s259 () Bool (distinct s0 s258))
[GOOD] (assert s259)
Looking for solution 129
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "@"))
[GOOD] (define-fun s260 () String "@")
[GOOD] (define-fun s261 () Bool (distinct s0 s260))
[GOOD] (assert s261)
Looking for solution 130
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "`"))
[GOOD] (define-fun s262 () String "`")
[GOOD] (define-fun s263 () Bool (distinct s0 s262))
[GOOD] (assert s263)
Looking for solution 131
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "A"))
[GOOD] (define-fun s264 () String "A")
[GOOD] (define-fun s265 () Bool (distinct s0 s264))
[GOOD] (assert s265)
Looking for solution 132
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "a"))
[GOOD] (define-fun s266 () String "a")
[GOOD] (define-fun s267 () Bool (distinct s0 s266))
[GOOD] (assert s267)
Looking for solution 133
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "P"))
[GOOD] (define-fun s268 () String "P")
[GOOD] (define-fun s269 () Bool (distinct s0 s268))
[GOOD] (assert s269)
Looking for solution 134
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "p"))
[GOOD] (define-fun s270 () String "p")
[GOOD] (define-fun s271 () Bool (distinct s0 s270))
[GOOD] (assert s271)
Looking for solution 135
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "Q"))
[GOOD] (define-fun s272 () String "Q")
[GOOD] (define-fun s273 () Bool (distinct s0 s272))
[GOOD] (assert s273)
Looking for solution 136
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "q"))
[GOOD] (define-fun s274 () String "q")
[GOOD] (define-fun s275 () Bool (distinct s0 s274))
[GOOD] (assert s275)
Looking for solution 137
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "H"))
[GOOD] (define-fun s276 () String "H")
[GOOD] (define-fun s277 () Bool (distinct s0 s276))
[GOOD] (assert s277)
Looking for solution 138
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "h"))
[GOOD] (define-fun s278 () String "h")
[GOOD] (define-fun s279 () Bool (distinct s0 s278))
[GOOD] (assert s279)
Looking for solution 139
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "I"))
[GOOD] (define-fun s280 () String "I")
[GOOD] (define-fun s281 () Bool (distinct s0 s280))
[GOOD] (assert s281)
Looking for solution 140
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "i"))
[GOOD] (define-fun s282 () String "i")
[GOOD] (define-fun s283 () Bool (distinct s0 s282))
[GOOD] (assert s283)
Looking for solution 141
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "X"))
[GOOD] (define-fun s284 () String "X")
[GOOD] (define-fun s285 () Bool (distinct s0 s284))
[GOOD] (assert s285)
Looking for solution 142
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "x"))
[GOOD] (define-fun s286 () String "x")
[GOOD] (define-fun s287 () Bool (distinct s0 s286))
[GOOD] (assert s287)
Looking for solution 143
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "Y"))
[GOOD] (define-fun s288 () String "Y")
[GOOD] (define-fun s289 () Bool (distinct s0 s288))
[GOOD] (assert s289)
Looking for solution 144
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "y"))
[GOOD] (define-fun s290 () String "y")
[GOOD] (define-fun s291 () Bool (distinct s0 s290))
[GOOD] (assert s291)
Looking for solution 145
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "B"))
[GOOD] (define-fun s292 () String "B")
[GOOD] (define-fun s293 () Bool (distinct s0 s292))
[GOOD] (assert s293)
Looking for solution 146
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "b"))
[GOOD] (define-fun s294 () String "b")
[GOOD] (define-fun s295 () Bool (distinct s0 s294))
[GOOD] (assert s295)
Looking for solution 147
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "C"))
[GOOD] (define-fun s296 () String "C")
[GOOD] (define-fun s297 () Bool (distinct s0 s296))
[GOOD] (assert s297)
Looking for solution 148
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "c"))
[GOOD] (define-fun s298 () String "c")
[GOOD] (define-fun s299 () Bool (distinct s0 s298))
[GOOD] (assert s299)
Looking for solution 149
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "R"))
[GOOD] (define-fun s300 () String "R")
[GOOD] (define-fun s301 () Bool (distinct s0 s300))
[GOOD] (assert s301)
Looking for solution 150
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "r"))
[GOOD] (define-fun s302 () String "r")
[GOOD] (define-fun s303 () Bool (distinct s0 s302))
[GOOD] (assert s303)
Looking for solution 151
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "S"))
[GOOD] (define-fun s304 () String "S")
[GOOD] (define-fun s305 () Bool (distinct s0 s304))
[GOOD] (assert s305)
Looking for solution 152
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "s"))
[GOOD] (define-fun s306 () String "s")
[GOOD] (define-fun s307 () Bool (distinct s0 s306))
[GOOD] (assert s307)
Looking for solution 153
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "J"))
[GOOD] (define-fun s308 () String "J")
[GOOD] (define-fun s309 () Bool (distinct s0 s308))
[GOOD] (assert s309)
Looking for solution 154
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "j"))
[GOOD] (define-fun s310 () String "j")
[GOOD] (define-fun s311 () Bool (distinct s0 s310))
[GOOD] (assert s311)
Looking for solution 155
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "K"))
[GOOD] (define-fun s312 () String "K")
[GOOD] (define-fun s313 () Bool (distinct s0 s312))
[GOOD] (assert s313)
Looking for solution 156
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "k"))
[GOOD] (define-fun s314 () String "k")
[GOOD] (define-fun s315 () Bool (distinct s0 s314))
[GOOD] (assert s315)
Looking for solution 157
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "Z"))
[GOOD] (define-fun s316 () String "Z")
[GOOD] (define-fun s317 () Bool (distinct s0 s316))
[GOOD] (assert s317)
Looking for solution 158
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "z"))
[GOOD] (define-fun s318 () String "z")
[GOOD] (define-fun s319 () Bool (distinct s0 s318))
[GOOD] (assert s319)
Looking for solution 159
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "["))
[GOOD] (define-fun s320 () String "[")
[GOOD] (define-fun s321 () Bool (distinct s0 s320))
[GOOD] (assert s321)
Looking for solution 160
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "{"))
[GOOD] (define-fun s322 () String "{")
[GOOD] (define-fun s323 () Bool (distinct s0 s322))
[GOOD] (assert s323)
Looking for solution 161
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "D"))
[GOOD] (define-fun s324 () String "D")
[GOOD] (define-fun s325 () Bool (distinct s0 s324))
[GOOD] (assert s325)
Looking for solution 162
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "d"))
[GOOD] (define-fun s326 () String "d")
[GOOD] (define-fun s327 () Bool (distinct s0 s326))
[GOOD] (assert s327)
Looking for solution 163
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "E"))
[GOOD] (define-fun s328 () String "E")
[GOOD] (define-fun s329 () Bool (distinct s0 s328))
[GOOD] (assert s329)
Looking for solution 164
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "e"))
[GOOD] (define-fun s330 () String "e")
[GOOD] (define-fun s331 () Bool (distinct s0 s330))
[GOOD] (assert s331)
Looking for solution 165
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "T"))
[GOOD] (define-fun s332 () String "T")
[GOOD] (define-fun s333 () Bool (distinct s0 s332))
[GOOD] (assert s333)
Looking for solution 166
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "t"))
[GOOD] (define-fun s334 () String "t")
[GOOD] (define-fun s335 () Bool (distinct s0 s334))
[GOOD] (assert s335)
Looking for solution 167
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "U"))
[GOOD] (define-fun s336 () String "U")
[GOOD] (define-fun s337 () Bool (distinct s0 s336))
[GOOD] (assert s337)
Looking for solution 168
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "u"))
[GOOD] (define-fun s338 () String "u")
[GOOD] (define-fun s339 () Bool (distinct s0 s338))
[GOOD] (assert s339)
Looking for solution 169
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "L"))
[GOOD] (define-fun s340 () String "L")
[GOOD] (define-fun s341 () Bool (distinct s0 s340))
[GOOD] (assert s341)
Looking for solution 170
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "l"))
[GOOD] (define-fun s342 () String "l")
[GOOD] (define-fun s343 () Bool (distinct s0 s342))
[GOOD] (assert s343)
Looking for solution 171
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "M"))
[GOOD] (define-fun s344 () String "M")
[GOOD] (define-fun s345 () Bool (distinct s0 s344))
[GOOD] (assert s345)
Looking for solution 172
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "m"))
[GOOD] (define-fun s346 () String "m")
[GOOD] (define-fun s347 () Bool (distinct s0 s346))
[GOOD] (assert s347)
Looking for solution 173
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\\"))
[GOOD] (define-fun s348 () String "\\")
[GOOD] (define-fun s349 () Bool (distinct s0 s348))
[GOOD] (assert s349)
Looking for solution 174
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "|"))
[GOOD] (define-fun s350 () String "|")
[GOOD] (define-fun s351 () Bool (distinct s0 s350))
[GOOD] (assert s351)
Looking for solution 175
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "]"))
[GOOD] (define-fun s352 () String "]")
[GOOD] (define-fun s353 () Bool (distinct s0 s352))
[GOOD] (assert s353)
Looking for solution 176
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "}"))
[GOOD] (define-fun s354 () String "}")
[GOOD] (define-fun s355 () Bool (distinct s0 s354))
[GOOD] (assert s355)
Looking for solution 177
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "F"))
[GOOD] (define-fun s356 () String "F")
[GOOD] (define-fun s357 () Bool (distinct s0 s356))
[GOOD] (assert s357)
Looking for solution 178
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "f"))
[GOOD] (define-fun s358 () String "f")
[GOOD] (define-fun s359 () Bool (distinct s0 s358))
[GOOD] (assert s359)
Looking for solution 179
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "G"))
[GOOD] (define-fun s360 () String "G")
[GOOD] (define-fun s361 () Bool (distinct s0 s360))
[GOOD] (assert s361)
Looking for solution 180
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "g"))
[GOOD] (define-fun s362 () String "g")
[GOOD] (define-fun s363 () Bool (distinct s0 s362))
[GOOD] (assert s363)
Looking for solution 181
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "V"))
[GOOD] (define-fun s364 () String "V")
[GOOD] (define-fun s365 () Bool (distinct s0 s364))
[GOOD] (assert s365)
Looking for solution 182
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "v"))
[GOOD] (define-fun s366 () String "v")
[GOOD] (define-fun s367 () Bool (distinct s0 s366))
[GOOD] (assert s367)
Looking for solution 183
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "W"))
[GOOD] (define-fun s368 () String "W")
[GOOD] (define-fun s369 () Bool (distinct s0 s368))
[GOOD] (assert s369)
Looking for solution 184
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "w"))
[GOOD] (define-fun s370 () String "w")
[GOOD] (define-fun s371 () Bool (distinct s0 s370))
[GOOD] (assert s371)
Looking for solution 185
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "N"))
[GOOD] (define-fun s372 () String "N")
[GOOD] (define-fun s373 () Bool (distinct s0 s372))
[GOOD] (assert s373)
Looking for solution 186
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "n"))
[GOOD] (define-fun s374 () String "n")
[GOOD] (define-fun s375 () Bool (distinct s0 s374))
[GOOD] (assert s375)
Looking for solution 187
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "O"))
[GOOD] (define-fun s376 () String "O")
[GOOD] (define-fun s377 () Bool (distinct s0 s376))
[GOOD] (assert s377)
Looking for solution 188
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "o"))
[GOOD] (define-fun s378 () String "o")
[GOOD] (define-fun s379 () Bool (distinct s0 s378))
[GOOD] (assert s379)
Looking for solution 189
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "^"))
[GOOD] (define-fun s380 () String "^")
[GOOD] (define-fun s381 () Bool (distinct s0 s380))
[GOOD] (assert s381)
Looking for solution 190
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "~"))
[GOOD] (define-fun s382 () String "~")
[GOOD] (define-fun s383 () Bool (distinct s0 s382))
[GOOD] (assert s383)
Looking for solution 191
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "_"))
[GOOD] (define-fun s384 () String "_")
[GOOD] (define-fun s385 () Bool (distinct s0 s384))
[GOOD] (assert s385)
Looking for solution 192
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 ""))
[GOOD] (define-fun s386 () String "")
[GOOD] (define-fun s387 () Bool (distinct s0 s386))
[GOOD] (assert s387)
Looking for solution 193
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xc0"))
[GOOD] (define-fun s388 () String "\xc0")
[GOOD] (define-fun s389 () Bool (distinct s0 s388))
[GOOD] (assert s389)
Looking for solution 194
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xe0"))
[GOOD] (define-fun s390 () String "\xe0")
[GOOD] (define-fun s391 () Bool (distinct s0 s390))
[GOOD] (assert s391)
Looking for solution 195
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xc1"))
[GOOD] (define-fun s392 () String "\xc1")
[GOOD] (define-fun s393 () Bool (distinct s0 s392))
[GOOD] (assert s393)
Looking for solution 196
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xe1"))
[GOOD] (define-fun s394 () String "\xe1")
[GOOD] (define-fun s395 () Bool (distinct s0 s394))
[GOOD] (assert s395)
Looking for solution 197
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xd0"))
[GOOD] (define-fun s396 () String "\xd0")
[GOOD] (define-fun s397 () Bool (distinct s0 s396))
[GOOD] (assert s397)
Looking for solution 198
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xf0"))
[GOOD] (define-fun s398 () String "\xf0")
[GOOD] (define-fun s399 () Bool (distinct s0 s398))
[GOOD] (assert s399)
Looking for solution 199
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xd1"))
[GOOD] (define-fun s400 () String "\xd1")
[GOOD] (define-fun s401 () Bool (distinct s0 s400))
[GOOD] (assert s401)
Looking for solution 200
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xf1"))
[GOOD] (define-fun s402 () String "\xf1")
[GOOD] (define-fun s403 () Bool (distinct s0 s402))
[GOOD] (assert s403)
Looking for solution 201
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xc8"))
[GOOD] (define-fun s404 () String "\xc8")
[GOOD] (define-fun s405 () Bool (distinct s0 s404))
[GOOD] (assert s405)
Looking for solution 202
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xe8"))
[GOOD] (define-fun s406 () String "\xe8")
[GOOD] (define-fun s407 () Bool (distinct s0 s406))
[GOOD] (assert s407)
Looking for solution 203
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xc9"))
[GOOD] (define-fun s408 () String "\xc9")
[GOOD] (define-fun s409 () Bool (distinct s0 s408))
[GOOD] (assert s409)
Looking for solution 204
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xe9"))
[GOOD] (define-fun s410 () String "\xe9")
[GOOD] (define-fun s411 () Bool (distinct s0 s410))
[GOOD] (assert s411)
Looking for solution 205
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xd8"))
[GOOD] (define-fun s412 () String "\xd8")
[GOOD] (define-fun s413 () Bool (distinct s0 s412))
[GOOD] (assert s413)
Looking for solution 206
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xf8"))
[GOOD] (define-fun s414 () String "\xf8")
[GOOD] (define-fun s415 () Bool (distinct s0 s414))
[GOOD] (assert s415)
Looking for solution 207
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xd9"))
[GOOD] (define-fun s416 () String "\xd9")
[GOOD] (define-fun s417 () Bool (distinct s0 s416))
[GOOD] (assert s417)
Looking for solution 208
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xf9"))
[GOOD] (define-fun s418 () String "\xf9")
[GOOD] (define-fun s419 () Bool (distinct s0 s418))
[GOOD] (assert s419)
Looking for solution 209
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xc2"))
[GOOD] (define-fun s420 () String "\xc2")
[GOOD] (define-fun s421 () Bool (distinct s0 s420))
[GOOD] (assert s421)
Looking for solution 210
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xe2"))
[GOOD] (define-fun s422 () String "\xe2")
[GOOD] (define-fun s423 () Bool (distinct s0 s422))
[GOOD] (assert s423)
Looking for solution 211
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xc3"))
[GOOD] (define-fun s424 () String "\xc3")
[GOOD] (define-fun s425 () Bool (distinct s0 s424))
[GOOD] (assert s425)
Looking for solution 212
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xe3"))
[GOOD] (define-fun s426 () String "\xe3")
[GOOD] (define-fun s427 () Bool (distinct s0 s426))
[GOOD] (assert s427)
Looking for solution 213
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xd2"))
[GOOD] (define-fun s428 () String "\xd2")
[GOOD] (define-fun s429 () Bool (distinct s0 s428))
[GOOD] (assert s429)
Looking for solution 214
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xf2"))
[GOOD] (define-fun s430 () String "\xf2")
[GOOD] (define-fun s431 () Bool (distinct s0 s430))
[GOOD] (assert s431)
Looking for solution 215
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xd3"))
[GOOD] (define-fun s432 () String "\xd3")
[GOOD] (define-fun s433 () Bool (distinct s0 s432))
[GOOD] (assert s433)
Looking for solution 216
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xf3"))
[GOOD] (define-fun s434 () String "\xf3")
[GOOD] (define-fun s435 () Bool (distinct s0 s434))
[GOOD] (assert s435)
Looking for solution 217
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xca"))
[GOOD] (define-fun s436 () String "\xca")
[GOOD] (define-fun s437 () Bool (distinct s0 s436))
[GOOD] (assert s437)
Looking for solution 218
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xea"))
[GOOD] (define-fun s438 () String "\xea")
[GOOD] (define-fun s439 () Bool (distinct s0 s438))
[GOOD] (assert s439)
Looking for solution 219
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xcb"))
[GOOD] (define-fun s440 () String "\xcb")
[GOOD] (define-fun s441 () Bool (distinct s0 s440))
[GOOD] (assert s441)
Looking for solution 220
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xeb"))
[GOOD] (define-fun s442 () String "\xeb")
[GOOD] (define-fun s443 () Bool (distinct s0 s442))
[GOOD] (assert s443)
Looking for solution 221
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xda"))
[GOOD] (define-fun s444 () String "\xda")
[GOOD] (define-fun s445 () Bool (distinct s0 s444))
[GOOD] (assert s445)
Looking for solution 222
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xfa"))
[GOOD] (define-fun s446 () String "\xfa")
[GOOD] (define-fun s447 () Bool (distinct s0 s446))
[GOOD] (assert s447)
Looking for solution 223
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xdb"))
[GOOD] (define-fun s448 () String "\xdb")
[GOOD] (define-fun s449 () Bool (distinct s0 s448))
[GOOD] (assert s449)
Looking for solution 224
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xfb"))
[GOOD] (define-fun s450 () String "\xfb")
[GOOD] (define-fun s451 () Bool (distinct s0 s450))
[GOOD] (assert s451)
Looking for solution 225
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xc4"))
[GOOD] (define-fun s452 () String "\xc4")
[GOOD] (define-fun s453 () Bool (distinct s0 s452))
[GOOD] (assert s453)
Looking for solution 226
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xe4"))
[GOOD] (define-fun s454 () String "\xe4")
[GOOD] (define-fun s455 () Bool (distinct s0 s454))
[GOOD] (assert s455)
Looking for solution 227
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xc5"))
[GOOD] (define-fun s456 () String "\xc5")
[GOOD] (define-fun s457 () Bool (distinct s0 s456))
[GOOD] (assert s457)
Looking for solution 228
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xe5"))
[GOOD] (define-fun s458 () String "\xe5")
[GOOD] (define-fun s459 () Bool (distinct s0 s458))
[GOOD] (assert s459)
Looking for solution 229
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xd4"))
[GOOD] (define-fun s460 () String "\xd4")
[GOOD] (define-fun s461 () Bool (distinct s0 s460))
[GOOD] (assert s461)
Looking for solution 230
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xf4"))
[GOOD] (define-fun s462 () String "\xf4")
[GOOD] (define-fun s463 () Bool (distinct s0 s462))
[GOOD] (assert s463)
Looking for solution 231
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xd5"))
[GOOD] (define-fun s464 () String "\xd5")
[GOOD] (define-fun s465 () Bool (distinct s0 s464))
[GOOD] (assert s465)
Looking for solution 232
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xf5"))
[GOOD] (define-fun s466 () String "\xf5")
[GOOD] (define-fun s467 () Bool (distinct s0 s466))
[GOOD] (assert s467)
Looking for solution 233
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xcc"))
[GOOD] (define-fun s468 () String "\xcc")
[GOOD] (define-fun s469 () Bool (distinct s0 s468))
[GOOD] (assert s469)
Looking for solution 234
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xec"))
[GOOD] (define-fun s470 () String "\xec")
[GOOD] (define-fun s471 () Bool (distinct s0 s470))
[GOOD] (assert s471)
Looking for solution 235
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xcd"))
[GOOD] (define-fun s472 () String "\xcd")
[GOOD] (define-fun s473 () Bool (distinct s0 s472))
[GOOD] (assert s473)
Looking for solution 236
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xed"))
[GOOD] (define-fun s474 () String "\xed")
[GOOD] (define-fun s475 () Bool (distinct s0 s474))
[GOOD] (assert s475)
Looking for solution 237
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xdc"))
[GOOD] (define-fun s476 () String "\xdc")
[GOOD] (define-fun s477 () Bool (distinct s0 s476))
[GOOD] (assert s477)
Looking for solution 238
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xfc"))
[GOOD] (define-fun s478 () String "\xfc")
[GOOD] (define-fun s479 () Bool (distinct s0 s478))
[GOOD] (assert s479)
Looking for solution 239
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xdd"))
[GOOD] (define-fun s480 () String "\xdd")
[GOOD] (define-fun s481 () Bool (distinct s0 s480))
[GOOD] (assert s481)
Looking for solution 240
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xfd"))
[GOOD] (define-fun s482 () String "\xfd")
[GOOD] (define-fun s483 () Bool (distinct s0 s482))
[GOOD] (assert s483)
Looking for solution 241
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xc6"))
[GOOD] (define-fun s484 () String "\xc6")
[GOOD] (define-fun s485 () Bool (distinct s0 s484))
[GOOD] (assert s485)
Looking for solution 242
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xe6"))
[GOOD] (define-fun s486 () String "\xe6")
[GOOD] (define-fun s487 () Bool (distinct s0 s486))
[GOOD] (assert s487)
Looking for solution 243
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xc7"))
[GOOD] (define-fun s488 () String "\xc7")
[GOOD] (define-fun s489 () Bool (distinct s0 s488))
[GOOD] (assert s489)
Looking for solution 244
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xe7"))
[GOOD] (define-fun s490 () String "\xe7")
[GOOD] (define-fun s491 () Bool (distinct s0 s490))
[GOOD] (assert s491)
Looking for solution 245
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xd6"))
[GOOD] (define-fun s492 () String "\xd6")
[GOOD] (define-fun s493 () Bool (distinct s0 s492))
[GOOD] (assert s493)
Looking for solution 246
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xf6"))
[GOOD] (define-fun s494 () String "\xf6")
[GOOD] (define-fun s495 () Bool (distinct s0 s494))
[GOOD] (assert s495)
Looking for solution 247
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xd7"))
[GOOD] (define-fun s496 () String "\xd7")
[GOOD] (define-fun s497 () Bool (distinct s0 s496))
[GOOD] (assert s497)
Looking for solution 248
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xf7"))
[GOOD] (define-fun s498 () String "\xf7")
[GOOD] (define-fun s499 () Bool (distinct s0 s498))
[GOOD] (assert s499)
Looking for solution 249
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xce"))
[GOOD] (define-fun s500 () String "\xce")
[GOOD] (define-fun s501 () Bool (distinct s0 s500))
[GOOD] (assert s501)
Looking for solution 250
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xee"))
[GOOD] (define-fun s502 () String "\xee")
[GOOD] (define-fun s503 () Bool (distinct s0 s502))
[GOOD] (assert s503)
Looking for solution 251
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xcf"))
[GOOD] (define-fun s504 () String "\xcf")
[GOOD] (define-fun s505 () Bool (distinct s0 s504))
[GOOD] (assert s505)
Looking for solution 252
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xef"))
[GOOD] (define-fun s506 () String "\xef")
[GOOD] (define-fun s507 () Bool (distinct s0 s506))
[GOOD] (assert s507)
Looking for solution 253
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xde"))
[GOOD] (define-fun s508 () String "\xde")
[GOOD] (define-fun s509 () Bool (distinct s0 s508))
[GOOD] (assert s509)
Looking for solution 254
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xfe"))
[GOOD] (define-fun s510 () String "\xfe")
[GOOD] (define-fun s511 () Bool (distinct s0 s510))
[GOOD] (assert s511)
Looking for solution 255
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xdf"))
[GOOD] (define-fun s512 () String "\xdf")
[GOOD] (define-fun s513 () Bool (distinct s0 s512))
[GOOD] (assert s513)
Looking for solution 256
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 "\xff"))
[GOOD] (define-fun s514 () String "\xff")
[GOOD] (define-fun s515 () Bool (distinct s0 s514))
[GOOD] (assert s515)
Looking for solution 257
[SEND] (check-sat)
[RECV] unsat
*** Solver   : Z3
*** Exit code: ExitSuccess