import angr
import claripy

p = angr.Project('quad2_wicked')
s = p.factory.simulation_manager()

#BVS -> bit vector symbolic
#BVV -> bit vector value

x = claripy.BVS('x', 32)

class my_scanf(angr.SimProcedure):
	def run(self, fmt, ptr):
		self.state.mem[ptr].dword = x

p.hook_symbol('__isoc99_scanf', my_scanf(), replace=True)

base_addr = 0x400000

#goto_addr = 0x120e + base_addr
#avoid_addr= 0x1226 + base_addr

goto_addr = 0x11db + base_addr
avoid_addr= 0x11f3 + base_addr

s.explore(find=goto_addr, avoid=avoid_addr)

#s.explore(avoid=lambda q: b"almost" in q.posix.dumps(1))

#for i in s.found:
#	print i.solver.eval(x)


#print s.found[0].solver.max(x)

res=[]

for i in range(1, 10):
	try:
		res = s.found[0].solver.eval_atleast(x, i)
	except:
		break

print res


for i in range(0, 10):
	try:
		xVal =  s.found[0].solver.eval(x)
		print xVal
		s.found[0].solver.add(x != xVal)
	except:
		break

