A Z3Py example on getting all possible models and adjusting results.

get-models.py

from z3 import *
import binascii

zs             = Solver()
findInputLen   = 19
findInput      = [BitVec("findInput[%d]" % i,8)for i in range(0,findInputLen)]
SumInt         = BitVec("SumInt",32)

forbiddenCharsList = "|}{\\/\"\'!@#%^&*()=+- ,;~><`:.[]"

# if any string from the toFind string list found in a model
# it will be set as a constat part in next models 
toFind         = ["l337","_1s_","0bf","u$c4"] 

# acceptable model character range
charSetStart = 0x20 
charSetEnd   = 0x7f

# set model character range
def charsetRange(charSetStart,charSetEnd):
	# define basic range
	for i in range(0,len(findInput)): 
		zs.add(findInput[i] >= charSetStart)
		zs.add(findInput[i] <= charSetEnd)

# set character to exclude 
def forbiddenChars(forbiddenCharsList):
	for i in range(0,len(findInput)):
		for j in list(forbiddenCharsList): 
			zs.add(findInput[i] != ord(j))

def findStr(flagstr,toFind):
	for i in toFind:
		if i in flagstr:
			index = flagstr.find(i)
			mindex = 0
			for j in range(len(i)):
				zs.add(findInput[index+mindex] == ord(i[mindex]))
				mindex +=1

# set Z3 rules
def ruleflag():

	# Z3 conditions goes here 
	# =======================
	zs.add((findInput[2] & 0xf) <= findInput[15] >> 1)
	zs.add((findInput[15] >> 1) - (findInput[2] & 0xf) == findInput[0])
	zs.add(findInput[17] + findInput[16] == findInput[2])
	zs.add(findInput[1] >> 1 == findInput[12])
	zs.add((findInput[10] ^ findInput[11]) == findInput[8])
	zs.add((findInput[13] - findInput[4] == findInput[14] - (findInput[6] - findInput[4])))
	zs.add((((findInput[3] - findInput[9]) & 0xff) >> 4 | ((findInput[3] - findInput[9]) & 0xf) << 4) == findInput[7])
	zs.add((findInput[15] >> 1 ^ 0x55) == findInput[5])
	zs.add((((findInput[1]) & 0xff) >> 4 | ((findInput[1]) & 0xf) << 4) == findInput[4] + 2)
	zs.add((findInput[18] << 1) / 3 == findInput[4])
	zs.add((findInput[13] >> 4) + findInput[0] == findInput[18])
	zs.add(findInput[4] + findInput[6] + findInput[8] == 0x89)
	zs.add(findInput[9] + findInput[5] + findInput[7] == 0xe7)
	# ========================


	# convert BitVector to Int (was part from the CTF challenge)
	Index  = 9
	SumInt = 0
	while True:
		Index = Index + 1
		SumInt = BV2Int(findInput[Index]) + SumInt
		if Index == 0x12:
			break
	zs.add(SumInt == 0x2d9)


# get all models 
def getmodels():
	while True:
		ruleflag()	 
		# if z3 found a solution 
		if zs.check() == sat: 
			# print it 
			flag = ""
			for i in range(0,len(findInput)):
				final = int(str(zs.model()[findInput[i]]))
				flag += chr(final)
			print("Flag Is: " + flag)

			findStr(flag,toFind)
			# tell Z3 to get all models except the just found one
			zs.add(Or([sym() != zs.model()[sym] for sym in zs.model().decls()]))
		else:
			print("No more models found")
			break

if __name__ == "__main__":
	charsetRange(charSetStart,charSetEnd)
	forbiddenChars(forbiddenCharsList)
	getmodels()