Skip to content

Instantly share code, notes, and snippets.

@sudhackar

sudhackar/quad-crackme.py

Last active May 23, 2018 10:29
Show Gist options
  • Save sudhackar/80fbe0d670d727e42bb481cfd11174de to your computer and use it in GitHub Desktop.
Save sudhackar/80fbe0d670d727e42bb481cfd11174de to your computer and use it in GitHub Desktop.
Download ZIP
Source for Nullcon HackIM 2018 RE 150 Quad Math
Raw
quad-crackme.py
def genf(a,b,i):
stub = '''void f%d(){ // %c - %c
if (((int)(flag[%d])*(int)(flag[%d]) + %d * (int)(flag[%d]) + %d ) || ((int)(flag[%d])*(int)(flag[%d]) + %d * (int)(flag[%d]) + %d )){
fin = 1;
}
else{
fin = 0;
}
}'''
print stub % ( i, chr(a), chr(b), i, i, (-(a+b)), i, (a*b), i+2, i+2, (-(a+b)), i+2, (a*b))
flag = raw_input().strip()
print '''#include <stdio.h>
int fin = 1;
char flag[%d] ;//%s;
''' % (len(flag), flag)
for i in xrange(0, len(flag) - 2):
genf(ord(flag[i]),ord(flag[i+2]),i)
print '''int main(int argc, char **argv)
{
scanf("%s", flag);
'''
for i in xrange(len(flag)-2):
print "f%d();" % (i)
print ''' printf("%d",fin);
return 0;
}'''
Raw
release.c
#include <stdio.h>
int fin = 1;
char flag[68] ;//hackim18{'W0W_wow_w0w_WoW_y0u_h4v3_m4th_sk1ll5_W0oW_w0ow_wo0w_Wo0W'};
void f0(){ // h - c
if (((int)(flag[0])*(int)(flag[0]) + -203 * (int)(flag[0]) + 10296 ) || ((int)(flag[2])*(int)(flag[2]) + -203 * (int)(flag[2]) + 10296 )){
fin = 1;
}
else{
fin = 0;
}
}
void f1(){ // a - k
if (((int)(flag[1])*(int)(flag[1]) + -204 * (int)(flag[1]) + 10379 ) || ((int)(flag[3])*(int)(flag[3]) + -204 * (int)(flag[3]) + 10379 )){
fin = 1;
}
else{
fin = 0;
}
}
void f2(){ // c - i
if (((int)(flag[2])*(int)(flag[2]) + -204 * (int)(flag[2]) + 10395 ) || ((int)(flag[4])*(int)(flag[4]) + -204 * (int)(flag[4]) + 10395 )){
fin = 1;
}
else{
fin = 0;
}
}
void f3(){ // k - m
if (((int)(flag[3])*(int)(flag[3]) + -216 * (int)(flag[3]) + 11663 ) || ((int)(flag[5])*(int)(flag[5]) + -216 * (int)(flag[5]) + 11663 )){
fin = 1;
}
else{
fin = 0;
}
}
void f4(){ // i - 1
if (((int)(flag[4])*(int)(flag[4]) + -154 * (int)(flag[4]) + 5145 ) || ((int)(flag[6])*(int)(flag[6]) + -154 * (int)(flag[6]) + 5145 )){
fin = 1;
}
else{
fin = 0;
}
}
void f5(){ // m - 8
if (((int)(flag[5])*(int)(flag[5]) + -165 * (int)(flag[5]) + 6104 ) || ((int)(flag[7])*(int)(flag[7]) + -165 * (int)(flag[7]) + 6104 )){
fin = 1;
}
else{
fin = 0;
}
}
void f6(){ // 1 - {
if (((int)(flag[6])*(int)(flag[6]) + -172 * (int)(flag[6]) + 6027 ) || ((int)(flag[8])*(int)(flag[8]) + -172 * (int)(flag[8]) + 6027 )){
fin = 1;
}
else{
fin = 0;
}
}
void f7(){ // 8 - '
if (((int)(flag[7])*(int)(flag[7]) + -95 * (int)(flag[7]) + 2184 ) || ((int)(flag[9])*(int)(flag[9]) + -95 * (int)(flag[9]) + 2184 )){
fin = 1;
}
else{
fin = 0;
}
}
void f8(){ // { - W
if (((int)(flag[8])*(int)(flag[8]) + -210 * (int)(flag[8]) + 10701 ) || ((int)(flag[10])*(int)(flag[10]) + -210 * (int)(flag[10]) + 10701 )){
fin = 1;
}
else{
fin = 0;
}
}
void f9(){ // ' - 0
if (((int)(flag[9])*(int)(flag[9]) + -87 * (int)(flag[9]) + 1872 ) || ((int)(flag[11])*(int)(flag[11]) + -87 * (int)(flag[11]) + 1872 )){
fin = 1;
}
else{
fin = 0;
}
}
void f10(){ // W - W
if (((int)(flag[10])*(int)(flag[10]) + -174 * (int)(flag[10]) + 7569 ) || ((int)(flag[12])*(int)(flag[12]) + -174 * (int)(flag[12]) + 7569 )){
fin = 1;
}
else{
fin = 0;
}
}
void f11(){ // 0 - _
if (((int)(flag[11])*(int)(flag[11]) + -143 * (int)(flag[11]) + 4560 ) || ((int)(flag[13])*(int)(flag[13]) + -143 * (int)(flag[13]) + 4560 )){
fin = 1;
}
else{
fin = 0;
}
}
void f12(){ // W - w
if (((int)(flag[12])*(int)(flag[12]) + -206 * (int)(flag[12]) + 10353 ) || ((int)(flag[14])*(int)(flag[14]) + -206 * (int)(flag[14]) + 10353 )){
fin = 1;
}
else{
fin = 0;
}
}
void f13(){ // _ - o
if (((int)(flag[13])*(int)(flag[13]) + -206 * (int)(flag[13]) + 10545 ) || ((int)(flag[15])*(int)(flag[15]) + -206 * (int)(flag[15]) + 10545 )){
fin = 1;
}
else{
fin = 0;
}
}
void f14(){ // w - w
if (((int)(flag[14])*(int)(flag[14]) + -238 * (int)(flag[14]) + 14161 ) || ((int)(flag[16])*(int)(flag[16]) + -238 * (int)(flag[16]) + 14161 )){
fin = 1;
}
else{
fin = 0;
}
}
void f15(){ // o - _
if (((int)(flag[15])*(int)(flag[15]) + -206 * (int)(flag[15]) + 10545 ) || ((int)(flag[17])*(int)(flag[17]) + -206 * (int)(flag[17]) + 10545 )){
fin = 1;
}
else{
fin = 0;
}
}
void f16(){ // w - w
if (((int)(flag[16])*(int)(flag[16]) + -238 * (int)(flag[16]) + 14161 ) || ((int)(flag[18])*(int)(flag[18]) + -238 * (int)(flag[18]) + 14161 )){
fin = 1;
}
else{
fin = 0;
}
}
void f17(){ // _ - 0
if (((int)(flag[17])*(int)(flag[17]) + -143 * (int)(flag[17]) + 4560 ) || ((int)(flag[19])*(int)(flag[19]) + -143 * (int)(flag[19]) + 4560 )){
fin = 1;
}
else{
fin = 0;
}
}
void f18(){ // w - w
if (((int)(flag[18])*(int)(flag[18]) + -238 * (int)(flag[18]) + 14161 ) || ((int)(flag[20])*(int)(flag[20]) + -238 * (int)(flag[20]) + 14161 )){
fin = 1;
}
else{
fin = 0;
}
}
void f19(){ // 0 - _
if (((int)(flag[19])*(int)(flag[19]) + -143 * (int)(flag[19]) + 4560 ) || ((int)(flag[21])*(int)(flag[21]) + -143 * (int)(flag[21]) + 4560 )){
fin = 1;
}
else{
fin = 0;
}
}
void f20(){ // w - W
if (((int)(flag[20])*(int)(flag[20]) + -206 * (int)(flag[20]) + 10353 ) || ((int)(flag[22])*(int)(flag[22]) + -206 * (int)(flag[22]) + 10353 )){
fin = 1;
}
else{
fin = 0;
}
}
void f21(){ // _ - o
if (((int)(flag[21])*(int)(flag[21]) + -206 * (int)(flag[21]) + 10545 ) || ((int)(flag[23])*(int)(flag[23]) + -206 * (int)(flag[23]) + 10545 )){
fin = 1;
}
else{
fin = 0;
}
}
void f22(){ // W - W
if (((int)(flag[22])*(int)(flag[22]) + -174 * (int)(flag[22]) + 7569 ) || ((int)(flag[24])*(int)(flag[24]) + -174 * (int)(flag[24]) + 7569 )){
fin = 1;
}
else{
fin = 0;
}
}
void f23(){ // o - _
if (((int)(flag[23])*(int)(flag[23]) + -206 * (int)(flag[23]) + 10545 ) || ((int)(flag[25])*(int)(flag[25]) + -206 * (int)(flag[25]) + 10545 )){
fin = 1;
}
else{
fin = 0;
}
}
void f24(){ // W - y
if (((int)(flag[24])*(int)(flag[24]) + -208 * (int)(flag[24]) + 10527 ) || ((int)(flag[26])*(int)(flag[26]) + -208 * (int)(flag[26]) + 10527 )){
fin = 1;
}
else{
fin = 0;
}
}
void f25(){ // _ - 0
if (((int)(flag[25])*(int)(flag[25]) + -143 * (int)(flag[25]) + 4560 ) || ((int)(flag[27])*(int)(flag[27]) + -143 * (int)(flag[27]) + 4560 )){
fin = 1;
}
else{
fin = 0;
}
}
void f26(){ // y - u
if (((int)(flag[26])*(int)(flag[26]) + -238 * (int)(flag[26]) + 14157 ) || ((int)(flag[28])*(int)(flag[28]) + -238 * (int)(flag[28]) + 14157 )){
fin = 1;
}
else{
fin = 0;
}
}
void f27(){ // 0 - _
if (((int)(flag[27])*(int)(flag[27]) + -143 * (int)(flag[27]) + 4560 ) || ((int)(flag[29])*(int)(flag[29]) + -143 * (int)(flag[29]) + 4560 )){
fin = 1;
}
else{
fin = 0;
}
}
void f28(){ // u - h
if (((int)(flag[28])*(int)(flag[28]) + -221 * (int)(flag[28]) + 12168 ) || ((int)(flag[30])*(int)(flag[30]) + -221 * (int)(flag[30]) + 12168 )){
fin = 1;
}
else{
fin = 0;
}
}
void f29(){ // _ - 4
if (((int)(flag[29])*(int)(flag[29]) + -147 * (int)(flag[29]) + 4940 ) || ((int)(flag[31])*(int)(flag[31]) + -147 * (int)(flag[31]) + 4940 )){
fin = 1;
}
else{
fin = 0;
}
}
void f30(){ // h - v
if (((int)(flag[30])*(int)(flag[30]) + -222 * (int)(flag[30]) + 12272 ) || ((int)(flag[32])*(int)(flag[32]) + -222 * (int)(flag[32]) + 12272 )){
fin = 1;
}
else{
fin = 0;
}
}
void f31(){ // 4 - 3
if (((int)(flag[31])*(int)(flag[31]) + -103 * (int)(flag[31]) + 2652 ) || ((int)(flag[33])*(int)(flag[33]) + -103 * (int)(flag[33]) + 2652 )){
fin = 1;
}
else{
fin = 0;
}
}
void f32(){ // v - _
if (((int)(flag[32])*(int)(flag[32]) + -213 * (int)(flag[32]) + 11210 ) || ((int)(flag[34])*(int)(flag[34]) + -213 * (int)(flag[34]) + 11210 )){
fin = 1;
}
else{
fin = 0;
}
}
void f33(){ // 3 - m
if (((int)(flag[33])*(int)(flag[33]) + -160 * (int)(flag[33]) + 5559 ) || ((int)(flag[35])*(int)(flag[35]) + -160 * (int)(flag[35]) + 5559 )){
fin = 1;
}
else{
fin = 0;
}
}
void f34(){ // _ - 4
if (((int)(flag[34])*(int)(flag[34]) + -147 * (int)(flag[34]) + 4940 ) || ((int)(flag[36])*(int)(flag[36]) + -147 * (int)(flag[36]) + 4940 )){
fin = 1;
}
else{
fin = 0;
}
}
void f35(){ // m - t
if (((int)(flag[35])*(int)(flag[35]) + -225 * (int)(flag[35]) + 12644 ) || ((int)(flag[37])*(int)(flag[37]) + -225 * (int)(flag[37]) + 12644 )){
fin = 1;
}
else{
fin = 0;
}
}
void f36(){ // 4 - h
if (((int)(flag[36])*(int)(flag[36]) + -156 * (int)(flag[36]) + 5408 ) || ((int)(flag[38])*(int)(flag[38]) + -156 * (int)(flag[38]) + 5408 )){
fin = 1;
}
else{
fin = 0;
}
}
void f37(){ // t - _
if (((int)(flag[37])*(int)(flag[37]) + -211 * (int)(flag[37]) + 11020 ) || ((int)(flag[39])*(int)(flag[39]) + -211 * (int)(flag[39]) + 11020 )){
fin = 1;
}
else{
fin = 0;
}
}
void f38(){ // h - s
if (((int)(flag[38])*(int)(flag[38]) + -219 * (int)(flag[38]) + 11960 ) || ((int)(flag[40])*(int)(flag[40]) + -219 * (int)(flag[40]) + 11960 )){
fin = 1;
}
else{
fin = 0;
}
}
void f39(){ // _ - k
if (((int)(flag[39])*(int)(flag[39]) + -202 * (int)(flag[39]) + 10165 ) || ((int)(flag[41])*(int)(flag[41]) + -202 * (int)(flag[41]) + 10165 )){
fin = 1;
}
else{
fin = 0;
}
}
void f40(){ // s - 1
if (((int)(flag[40])*(int)(flag[40]) + -164 * (int)(flag[40]) + 5635 ) || ((int)(flag[42])*(int)(flag[42]) + -164 * (int)(flag[42]) + 5635 )){
fin = 1;
}
else{
fin = 0;
}
}
void f41(){ // k - l
if (((int)(flag[41])*(int)(flag[41]) + -215 * (int)(flag[41]) + 11556 ) || ((int)(flag[43])*(int)(flag[43]) + -215 * (int)(flag[43]) + 11556 )){
fin = 1;
}
else{
fin = 0;
}
}
void f42(){ // 1 - l
if (((int)(flag[42])*(int)(flag[42]) + -157 * (int)(flag[42]) + 5292 ) || ((int)(flag[44])*(int)(flag[44]) + -157 * (int)(flag[44]) + 5292 )){
fin = 1;
}
else{
fin = 0;
}
}
void f43(){ // l - 5
if (((int)(flag[43])*(int)(flag[43]) + -161 * (int)(flag[43]) + 5724 ) || ((int)(flag[45])*(int)(flag[45]) + -161 * (int)(flag[45]) + 5724 )){
fin = 1;
}
else{
fin = 0;
}
}
void f44(){ // l - _
if (((int)(flag[44])*(int)(flag[44]) + -203 * (int)(flag[44]) + 10260 ) || ((int)(flag[46])*(int)(flag[46]) + -203 * (int)(flag[46]) + 10260 )){
fin = 1;
}
else{
fin = 0;
}
}
void f45(){ // 5 - W
if (((int)(flag[45])*(int)(flag[45]) + -140 * (int)(flag[45]) + 4611 ) || ((int)(flag[47])*(int)(flag[47]) + -140 * (int)(flag[47]) + 4611 )){
fin = 1;
}
else{
fin = 0;
}
}
void f46(){ // _ - 0
if (((int)(flag[46])*(int)(flag[46]) + -143 * (int)(flag[46]) + 4560 ) || ((int)(flag[48])*(int)(flag[48]) + -143 * (int)(flag[48]) + 4560 )){
fin = 1;
}
else{
fin = 0;
}
}
void f47(){ // W - o
if (((int)(flag[47])*(int)(flag[47]) + -198 * (int)(flag[47]) + 9657 ) || ((int)(flag[49])*(int)(flag[49]) + -198 * (int)(flag[49]) + 9657 )){
fin = 1;
}
else{
fin = 0;
}
}
void f48(){ // 0 - W
if (((int)(flag[48])*(int)(flag[48]) + -135 * (int)(flag[48]) + 4176 ) || ((int)(flag[50])*(int)(flag[50]) + -135 * (int)(flag[50]) + 4176 )){
fin = 1;
}
else{
fin = 0;
}
}
void f49(){ // o - _
if (((int)(flag[49])*(int)(flag[49]) + -206 * (int)(flag[49]) + 10545 ) || ((int)(flag[51])*(int)(flag[51]) + -206 * (int)(flag[51]) + 10545 )){
fin = 1;
}
else{
fin = 0;
}
}
void f50(){ // W - w
if (((int)(flag[50])*(int)(flag[50]) + -206 * (int)(flag[50]) + 10353 ) || ((int)(flag[52])*(int)(flag[52]) + -206 * (int)(flag[52]) + 10353 )){
fin = 1;
}
else{
fin = 0;
}
}
void f51(){ // _ - 0
if (((int)(flag[51])*(int)(flag[51]) + -143 * (int)(flag[51]) + 4560 ) || ((int)(flag[53])*(int)(flag[53]) + -143 * (int)(flag[53]) + 4560 )){
fin = 1;
}
else{
fin = 0;
}
}
void f52(){ // w - o
if (((int)(flag[52])*(int)(flag[52]) + -230 * (int)(flag[52]) + 13209 ) || ((int)(flag[54])*(int)(flag[54]) + -230 * (int)(flag[54]) + 13209 )){
fin = 1;
}
else{
fin = 0;
}
}
void f53(){ // 0 - w
if (((int)(flag[53])*(int)(flag[53]) + -167 * (int)(flag[53]) + 5712 ) || ((int)(flag[55])*(int)(flag[55]) + -167 * (int)(flag[55]) + 5712 )){
fin = 1;
}
else{
fin = 0;
}
}
void f54(){ // o - _
if (((int)(flag[54])*(int)(flag[54]) + -206 * (int)(flag[54]) + 10545 ) || ((int)(flag[56])*(int)(flag[56]) + -206 * (int)(flag[56]) + 10545 )){
fin = 1;
}
else{
fin = 0;
}
}
void f55(){ // w - w
if (((int)(flag[55])*(int)(flag[55]) + -238 * (int)(flag[55]) + 14161 ) || ((int)(flag[57])*(int)(flag[57]) + -238 * (int)(flag[57]) + 14161 )){
fin = 1;
}
else{
fin = 0;
}
}
void f56(){ // _ - o
if (((int)(flag[56])*(int)(flag[56]) + -206 * (int)(flag[56]) + 10545 ) || ((int)(flag[58])*(int)(flag[58]) + -206 * (int)(flag[58]) + 10545 )){
fin = 1;
}
else{
fin = 0;
}
}
void f57(){ // w - 0
if (((int)(flag[57])*(int)(flag[57]) + -167 * (int)(flag[57]) + 5712 ) || ((int)(flag[59])*(int)(flag[59]) + -167 * (int)(flag[59]) + 5712 )){
fin = 1;
}
else{
fin = 0;
}
}
void f58(){ // o - w
if (((int)(flag[58])*(int)(flag[58]) + -230 * (int)(flag[58]) + 13209 ) || ((int)(flag[60])*(int)(flag[60]) + -230 * (int)(flag[60]) + 13209 )){
fin = 1;
}
else{
fin = 0;
}
}
void f59(){ // 0 - _
if (((int)(flag[59])*(int)(flag[59]) + -143 * (int)(flag[59]) + 4560 ) || ((int)(flag[61])*(int)(flag[61]) + -143 * (int)(flag[61]) + 4560 )){
fin = 1;
}
else{
fin = 0;
}
}
void f60(){ // w - W
if (((int)(flag[60])*(int)(flag[60]) + -206 * (int)(flag[60]) + 10353 ) || ((int)(flag[62])*(int)(flag[62]) + -206 * (int)(flag[62]) + 10353 )){
fin = 1;
}
else{
fin = 0;
}
}
void f61(){ // _ - o
if (((int)(flag[61])*(int)(flag[61]) + -206 * (int)(flag[61]) + 10545 ) || ((int)(flag[63])*(int)(flag[63]) + -206 * (int)(flag[63]) + 10545 )){
fin = 1;
}
else{
fin = 0;
}
}
void f62(){ // W - 0
if (((int)(flag[62])*(int)(flag[62]) + -135 * (int)(flag[62]) + 4176 ) || ((int)(flag[64])*(int)(flag[64]) + -135 * (int)(flag[64]) + 4176 )){
fin = 1;
}
else{
fin = 0;
}
}
void f63(){ // o - W
if (((int)(flag[63])*(int)(flag[63]) + -198 * (int)(flag[63]) + 9657 ) || ((int)(flag[65])*(int)(flag[65]) + -198 * (int)(flag[65]) + 9657 )){
fin = 1;
}
else{
fin = 0;
}
}
void f64(){ // 0 - '
if (((int)(flag[64])*(int)(flag[64]) + -87 * (int)(flag[64]) + 1872 ) || ((int)(flag[66])*(int)(flag[66]) + -87 * (int)(flag[66]) + 1872 )){
fin = 1;
}
else{
fin = 0;
}
}
void f65(){ // W - }
if (((int)(flag[65])*(int)(flag[65]) + -212 * (int)(flag[65]) + 10875 ) || ((int)(flag[67])*(int)(flag[67]) + -212 * (int)(flag[67]) + 10875 )){
fin = 1;
}
else{
fin = 0;
}
}
int main(int argc, char **argv)
{
scanf("%s", flag);
f0();
f1();
f2();
f3();
f4();
f5();
f6();
f7();
f8();
f9();
f10();
f11();
f12();
f13();
f14();
f15();
f16();
f17();
f18();
f19();
f20();
f21();
f22();
f23();
f24();
f25();
f26();
f27();
f28();
f29();
f30();
f31();
f32();
f33();
f34();
f35();
f36();
f37();
f38();
f39();
f40();
f41();
f42();
f43();
f44();
f45();
f46();
f47();
f48();
f49();
f50();
f51();
f52();
f53();
f54();
f55();
f56();
f57();
f58();
f59();
f60();
f61();
f62();
f63();
f64();
f65();
printf("%d",fin);
return 0;
}
Raw
solve.py
from subprocess import Popen, PIPE, STDOUT
import string
charset = string.uppercase+string.lowercase+string.digits+"{}'_"
candidates = [set() for i in xrange(66)]
# charset = "abcd"
for i in charset:
flag = i*68
p = Popen(['./a.out'], stdout=PIPE, stdin=PIPE, stderr=STDOUT)
stdout = p.communicate(input=flag)[0]
# print i," : ",stdout
for idx,c in enumerate(stdout):
if c == "0":
candidates[idx].add(i)
# print candidates
print "".join(candidates[0] - candidates[2]),
print "".join(candidates[1] - candidates[3]),
for i in xrange(63):
print "".join((candidates[i] & candidates[i+2])),
print "".join(candidates[64] - candidates[62]),
print "".join(candidates[65] - candidates[63]),
Raw
solve_klee.c
#include <stdio.h>
#include <klee/klee.h>
#include <stdint.h>
#include <assert.h>
int i;
int fin = 1;
char flag[68] ;//hackim18{'W0W_wow_w0w_WoW_y0u_h4v3_m4th_sk1ll5_W0oW_w0ow_wo0w_Wo0W'};
//hackim18{'W0W_w_w_w0w_W_W_y0u_h4v3_m4th_sk1ll5_W0oW_w0ow_wo0w_Wo0W'}
void f0(){ // h - c
if (((int)(flag[0])*(int)(flag[0]) + -203 * (int)(flag[0]) + 10296 ) || ((int)(flag[2])*(int)(flag[2]) + -203 * (int)(flag[2]) + 10296 )){
fin = 1;
}
else{
fin = 0;
}
}
void f1(){ // a - k
if (((int)(flag[1])*(int)(flag[1]) + -204 * (int)(flag[1]) + 10379 ) || ((int)(flag[3])*(int)(flag[3]) + -204 * (int)(flag[3]) + 10379 )){
fin = 1;
}
else{
fin = 0;
}
}
void f2(){ // c - i
if (((int)(flag[2])*(int)(flag[2]) + -204 * (int)(flag[2]) + 10395 ) || ((int)(flag[4])*(int)(flag[4]) + -204 * (int)(flag[4]) + 10395 )){
fin = 1;
}
else{
fin = 0;
}
}
void f3(){ // k - m
if (((int)(flag[3])*(int)(flag[3]) + -216 * (int)(flag[3]) + 11663 ) || ((int)(flag[5])*(int)(flag[5]) + -216 * (int)(flag[5]) + 11663 )){
fin = 1;
}
else{
fin = 0;
}
}
void f4(){ // i - 1
if (((int)(flag[4])*(int)(flag[4]) + -154 * (int)(flag[4]) + 5145 ) || ((int)(flag[6])*(int)(flag[6]) + -154 * (int)(flag[6]) + 5145 )){
fin = 1;
}
else{
fin = 0;
}
}
void f5(){ // m - 8
if (((int)(flag[5])*(int)(flag[5]) + -165 * (int)(flag[5]) + 6104 ) || ((int)(flag[7])*(int)(flag[7]) + -165 * (int)(flag[7]) + 6104 )){
fin = 1;
}
else{
fin = 0;
}
}
void f6(){ // 1 - {
if (((int)(flag[6])*(int)(flag[6]) + -172 * (int)(flag[6]) + 6027 ) || ((int)(flag[8])*(int)(flag[8]) + -172 * (int)(flag[8]) + 6027 )){
fin = 1;
}
else{
fin = 0;
}
}
void f7(){ // 8 - '
if (((int)(flag[7])*(int)(flag[7]) + -95 * (int)(flag[7]) + 2184 ) || ((int)(flag[9])*(int)(flag[9]) + -95 * (int)(flag[9]) + 2184 )){
fin = 1;
}
else{
fin = 0;
}
}
void f8(){ // { - W
if (((int)(flag[8])*(int)(flag[8]) + -210 * (int)(flag[8]) + 10701 ) || ((int)(flag[10])*(int)(flag[10]) + -210 * (int)(flag[10]) + 10701 )){
fin = 1;
}
else{
fin = 0;
}
}
void f9(){ // ' - 0
if (((int)(flag[9])*(int)(flag[9]) + -87 * (int)(flag[9]) + 1872 ) || ((int)(flag[11])*(int)(flag[11]) + -87 * (int)(flag[11]) + 1872 )){
fin = 1;
}
else{
fin = 0;
}
}
void f10(){ // W - W
if (((int)(flag[10])*(int)(flag[10]) + -174 * (int)(flag[10]) + 7569 ) || ((int)(flag[12])*(int)(flag[12]) + -174 * (int)(flag[12]) + 7569 )){
fin = 1;
}
else{
fin = 0;
}
}
void f11(){ // 0 - _
if (((int)(flag[11])*(int)(flag[11]) + -143 * (int)(flag[11]) + 4560 ) || ((int)(flag[13])*(int)(flag[13]) + -143 * (int)(flag[13]) + 4560 )){
fin = 1;
}
else{
fin = 0;
}
}
void f12(){ // W - w
if (((int)(flag[12])*(int)(flag[12]) + -206 * (int)(flag[12]) + 10353 ) || ((int)(flag[14])*(int)(flag[14]) + -206 * (int)(flag[14]) + 10353 )){
fin = 1;
}
else{
fin = 0;
}
}
void f13(){ // _ - o
if (((int)(flag[13])*(int)(flag[13]) + -206 * (int)(flag[13]) + 10545 ) || ((int)(flag[15])*(int)(flag[15]) + -206 * (int)(flag[15]) + 10545 )){
fin = 1;
}
else{
fin = 0;
}
}
void f14(){ // w - w
if (((int)(flag[14])*(int)(flag[14]) + -238 * (int)(flag[14]) + 14161 ) || ((int)(flag[16])*(int)(flag[16]) + -238 * (int)(flag[16]) + 14161 )){
fin = 1;
}
else{
fin = 0;
}
}
void f15(){ // o - _
if (((int)(flag[15])*(int)(flag[15]) + -206 * (int)(flag[15]) + 10545 ) || ((int)(flag[17])*(int)(flag[17]) + -206 * (int)(flag[17]) + 10545 )){
fin = 1;
}
else{
fin = 0;
}
}
void f16(){ // w - w
if (((int)(flag[16])*(int)(flag[16]) + -238 * (int)(flag[16]) + 14161 ) || ((int)(flag[18])*(int)(flag[18]) + -238 * (int)(flag[18]) + 14161 )){
fin = 1;
}
else{
fin = 0;
}
}
void f17(){ // _ - 0
if (((int)(flag[17])*(int)(flag[17]) + -143 * (int)(flag[17]) + 4560 ) || ((int)(flag[19])*(int)(flag[19]) + -143 * (int)(flag[19]) + 4560 )){
fin = 1;
}
else{
fin = 0;
}
}
void f18(){ // w - w
if (((int)(flag[18])*(int)(flag[18]) + -238 * (int)(flag[18]) + 14161 ) || ((int)(flag[20])*(int)(flag[20]) + -238 * (int)(flag[20]) + 14161 )){
fin = 1;
}
else{
fin = 0;
}
}
void f19(){ // 0 - _
if (((int)(flag[19])*(int)(flag[19]) + -143 * (int)(flag[19]) + 4560 ) || ((int)(flag[21])*(int)(flag[21]) + -143 * (int)(flag[21]) + 4560 )){
fin = 1;
}
else{
fin = 0;
}
}
void f20(){ // w - W
if (((int)(flag[20])*(int)(flag[20]) + -206 * (int)(flag[20]) + 10353 ) || ((int)(flag[22])*(int)(flag[22]) + -206 * (int)(flag[22]) + 10353 )){
fin = 1;
}
else{
fin = 0;
}
}
void f21(){ // _ - o
if (((int)(flag[21])*(int)(flag[21]) + -206 * (int)(flag[21]) + 10545 ) || ((int)(flag[23])*(int)(flag[23]) + -206 * (int)(flag[23]) + 10545 )){
fin = 1;
}
else{
fin = 0;
}
}
void f22(){ // W - W
if (((int)(flag[22])*(int)(flag[22]) + -174 * (int)(flag[22]) + 7569 ) || ((int)(flag[24])*(int)(flag[24]) + -174 * (int)(flag[24]) + 7569 )){
fin = 1;
}
else{
fin = 0;
}
}
void f23(){ // o - _
if (((int)(flag[23])*(int)(flag[23]) + -206 * (int)(flag[23]) + 10545 ) || ((int)(flag[25])*(int)(flag[25]) + -206 * (int)(flag[25]) + 10545 )){
fin = 1;
}
else{
fin = 0;
}
}
void f24(){ // W - y
if (((int)(flag[24])*(int)(flag[24]) + -208 * (int)(flag[24]) + 10527 ) || ((int)(flag[26])*(int)(flag[26]) + -208 * (int)(flag[26]) + 10527 )){
fin = 1;
}
else{
fin = 0;
}
}
void f25(){ // _ - 0
if (((int)(flag[25])*(int)(flag[25]) + -143 * (int)(flag[25]) + 4560 ) || ((int)(flag[27])*(int)(flag[27]) + -143 * (int)(flag[27]) + 4560 )){
fin = 1;
}
else{
fin = 0;
}
}
void f26(){ // y - u
if (((int)(flag[26])*(int)(flag[26]) + -238 * (int)(flag[26]) + 14157 ) || ((int)(flag[28])*(int)(flag[28]) + -238 * (int)(flag[28]) + 14157 )){
fin = 1;
}
else{
fin = 0;
}
}
void f27(){ // 0 - _
if (((int)(flag[27])*(int)(flag[27]) + -143 * (int)(flag[27]) + 4560 ) || ((int)(flag[29])*(int)(flag[29]) + -143 * (int)(flag[29]) + 4560 )){
fin = 1;
}
else{
fin = 0;
}
}
void f28(){ // u - h
if (((int)(flag[28])*(int)(flag[28]) + -221 * (int)(flag[28]) + 12168 ) || ((int)(flag[30])*(int)(flag[30]) + -221 * (int)(flag[30]) + 12168 )){
fin = 1;
}
else{
fin = 0;
}
}
void f29(){ // _ - 4
if (((int)(flag[29])*(int)(flag[29]) + -147 * (int)(flag[29]) + 4940 ) || ((int)(flag[31])*(int)(flag[31]) + -147 * (int)(flag[31]) + 4940 )){
fin = 1;
}
else{
fin = 0;
}
}
void f30(){ // h - v
if (((int)(flag[30])*(int)(flag[30]) + -222 * (int)(flag[30]) + 12272 ) || ((int)(flag[32])*(int)(flag[32]) + -222 * (int)(flag[32]) + 12272 )){
fin = 1;
}
else{
fin = 0;
}
}
void f31(){ // 4 - 3
if (((int)(flag[31])*(int)(flag[31]) + -103 * (int)(flag[31]) + 2652 ) || ((int)(flag[33])*(int)(flag[33]) + -103 * (int)(flag[33]) + 2652 )){
fin = 1;
}
else{
fin = 0;
}
}
void f32(){ // v - _
if (((int)(flag[32])*(int)(flag[32]) + -213 * (int)(flag[32]) + 11210 ) || ((int)(flag[34])*(int)(flag[34]) + -213 * (int)(flag[34]) + 11210 )){
fin = 1;
}
else{
fin = 0;
}
}
void f33(){ // 3 - m
if (((int)(flag[33])*(int)(flag[33]) + -160 * (int)(flag[33]) + 5559 ) || ((int)(flag[35])*(int)(flag[35]) + -160 * (int)(flag[35]) + 5559 )){
fin = 1;
}
else{
fin = 0;
}
}
void f34(){ // _ - 4
if (((int)(flag[34])*(int)(flag[34]) + -147 * (int)(flag[34]) + 4940 ) || ((int)(flag[36])*(int)(flag[36]) + -147 * (int)(flag[36]) + 4940 )){
fin = 1;
}
else{
fin = 0;
}
}
void f35(){ // m - t
if (((int)(flag[35])*(int)(flag[35]) + -225 * (int)(flag[35]) + 12644 ) || ((int)(flag[37])*(int)(flag[37]) + -225 * (int)(flag[37]) + 12644 )){
fin = 1;
}
else{
fin = 0;
}
}
void f36(){ // 4 - h
if (((int)(flag[36])*(int)(flag[36]) + -156 * (int)(flag[36]) + 5408 ) || ((int)(flag[38])*(int)(flag[38]) + -156 * (int)(flag[38]) + 5408 )){
fin = 1;
}
else{
fin = 0;
}
}
void f37(){ // t - _
if (((int)(flag[37])*(int)(flag[37]) + -211 * (int)(flag[37]) + 11020 ) || ((int)(flag[39])*(int)(flag[39]) + -211 * (int)(flag[39]) + 11020 )){
fin = 1;
}
else{
fin = 0;
}
}
void f38(){ // h - s
if (((int)(flag[38])*(int)(flag[38]) + -219 * (int)(flag[38]) + 11960 ) || ((int)(flag[40])*(int)(flag[40]) + -219 * (int)(flag[40]) + 11960 )){
fin = 1;
}
else{
fin = 0;
}
}
void f39(){ // _ - k
if (((int)(flag[39])*(int)(flag[39]) + -202 * (int)(flag[39]) + 10165 ) || ((int)(flag[41])*(int)(flag[41]) + -202 * (int)(flag[41]) + 10165 )){
fin = 1;
}
else{
fin = 0;
}
}
void f40(){ // s - 1
if (((int)(flag[40])*(int)(flag[40]) + -164 * (int)(flag[40]) + 5635 ) || ((int)(flag[42])*(int)(flag[42]) + -164 * (int)(flag[42]) + 5635 )){
fin = 1;
}
else{
fin = 0;
}
}
void f41(){ // k - l
if (((int)(flag[41])*(int)(flag[41]) + -215 * (int)(flag[41]) + 11556 ) || ((int)(flag[43])*(int)(flag[43]) + -215 * (int)(flag[43]) + 11556 )){
fin = 1;
}
else{
fin = 0;
}
}
void f42(){ // 1 - l
if (((int)(flag[42])*(int)(flag[42]) + -157 * (int)(flag[42]) + 5292 ) || ((int)(flag[44])*(int)(flag[44]) + -157 * (int)(flag[44]) + 5292 )){
fin = 1;
}
else{
fin = 0;
}
}
void f43(){ // l - 5
if (((int)(flag[43])*(int)(flag[43]) + -161 * (int)(flag[43]) + 5724 ) || ((int)(flag[45])*(int)(flag[45]) + -161 * (int)(flag[45]) + 5724 )){
fin = 1;
}
else{
fin = 0;
}
}
void f44(){ // l - _
if (((int)(flag[44])*(int)(flag[44]) + -203 * (int)(flag[44]) + 10260 ) || ((int)(flag[46])*(int)(flag[46]) + -203 * (int)(flag[46]) + 10260 )){
fin = 1;
}
else{
fin = 0;
}
}
void f45(){ // 5 - W
if (((int)(flag[45])*(int)(flag[45]) + -140 * (int)(flag[45]) + 4611 ) || ((int)(flag[47])*(int)(flag[47]) + -140 * (int)(flag[47]) + 4611 )){
fin = 1;
}
else{
fin = 0;
}
}
void f46(){ // _ - 0
if (((int)(flag[46])*(int)(flag[46]) + -143 * (int)(flag[46]) + 4560 ) || ((int)(flag[48])*(int)(flag[48]) + -143 * (int)(flag[48]) + 4560 )){
fin = 1;
}
else{
fin = 0;
}
}
void f47(){ // W - o
if (((int)(flag[47])*(int)(flag[47]) + -198 * (int)(flag[47]) + 9657 ) || ((int)(flag[49])*(int)(flag[49]) + -198 * (int)(flag[49]) + 9657 )){
fin = 1;
}
else{
fin = 0;
}
}
void f48(){ // 0 - W
if (((int)(flag[48])*(int)(flag[48]) + -135 * (int)(flag[48]) + 4176 ) || ((int)(flag[50])*(int)(flag[50]) + -135 * (int)(flag[50]) + 4176 )){
fin = 1;
}
else{
fin = 0;
}
}
void f49(){ // o - _
if (((int)(flag[49])*(int)(flag[49]) + -206 * (int)(flag[49]) + 10545 ) || ((int)(flag[51])*(int)(flag[51]) + -206 * (int)(flag[51]) + 10545 )){
fin = 1;
}
else{
fin = 0;
}
}
void f50(){ // W - w
if (((int)(flag[50])*(int)(flag[50]) + -206 * (int)(flag[50]) + 10353 ) || ((int)(flag[52])*(int)(flag[52]) + -206 * (int)(flag[52]) + 10353 )){
fin = 1;
}
else{
fin = 0;
}
}
void f51(){ // _ - 0
if (((int)(flag[51])*(int)(flag[51]) + -143 * (int)(flag[51]) + 4560 ) || ((int)(flag[53])*(int)(flag[53]) + -143 * (int)(flag[53]) + 4560 )){
fin = 1;
}
else{
fin = 0;
}
}
void f52(){ // w - o
if (((int)(flag[52])*(int)(flag[52]) + -230 * (int)(flag[52]) + 13209 ) || ((int)(flag[54])*(int)(flag[54]) + -230 * (int)(flag[54]) + 13209 )){
fin = 1;
}
else{
fin = 0;
}
}
void f53(){ // 0 - w
if (((int)(flag[53])*(int)(flag[53]) + -167 * (int)(flag[53]) + 5712 ) || ((int)(flag[55])*(int)(flag[55]) + -167 * (int)(flag[55]) + 5712 )){
fin = 1;
}
else{
fin = 0;
}
}
void f54(){ // o - _
if (((int)(flag[54])*(int)(flag[54]) + -206 * (int)(flag[54]) + 10545 ) || ((int)(flag[56])*(int)(flag[56]) + -206 * (int)(flag[56]) + 10545 )){
fin = 1;
}
else{
fin = 0;
}
}
void f55(){ // w - w
if (((int)(flag[55])*(int)(flag[55]) + -238 * (int)(flag[55]) + 14161 ) || ((int)(flag[57])*(int)(flag[57]) + -238 * (int)(flag[57]) + 14161 )){
fin = 1;
}
else{
fin = 0;
}
}
void f56(){ // _ - o
if (((int)(flag[56])*(int)(flag[56]) + -206 * (int)(flag[56]) + 10545 ) || ((int)(flag[58])*(int)(flag[58]) + -206 * (int)(flag[58]) + 10545 )){
fin = 1;
}
else{
fin = 0;
}
}
void f57(){ // w - 0
if (((int)(flag[57])*(int)(flag[57]) + -167 * (int)(flag[57]) + 5712 ) || ((int)(flag[59])*(int)(flag[59]) + -167 * (int)(flag[59]) + 5712 )){
fin = 1;
}
else{
fin = 0;
}
}
void f58(){ // o - w
if (((int)(flag[58])*(int)(flag[58]) + -230 * (int)(flag[58]) + 13209 ) || ((int)(flag[60])*(int)(flag[60]) + -230 * (int)(flag[60]) + 13209 )){
fin = 1;
}
else{
fin = 0;
}
}
void f59(){ // 0 - _
if (((int)(flag[59])*(int)(flag[59]) + -143 * (int)(flag[59]) + 4560 ) || ((int)(flag[61])*(int)(flag[61]) + -143 * (int)(flag[61]) + 4560 )){
fin = 1;
}
else{
fin = 0;
}
}
void f60(){ // w - W
if (((int)(flag[60])*(int)(flag[60]) + -206 * (int)(flag[60]) + 10353 ) || ((int)(flag[62])*(int)(flag[62]) + -206 * (int)(flag[62]) + 10353 )){
fin = 1;
}
else{
fin = 0;
}
}
void f61(){ // _ - o
if (((int)(flag[61])*(int)(flag[61]) + -206 * (int)(flag[61]) + 10545 ) || ((int)(flag[63])*(int)(flag[63]) + -206 * (int)(flag[63]) + 10545 )){
fin = 1;
}
else{
fin = 0;
}
}
void f62(){ // W - 0
if (((int)(flag[62])*(int)(flag[62]) + -135 * (int)(flag[62]) + 4176 ) || ((int)(flag[64])*(int)(flag[64]) + -135 * (int)(flag[64]) + 4176 )){
fin = 1;
}
else{
fin = 0;
}
}
void f63(){ // o - W
if (((int)(flag[63])*(int)(flag[63]) + -198 * (int)(flag[63]) + 9657 ) || ((int)(flag[65])*(int)(flag[65]) + -198 * (int)(flag[65]) + 9657 )){
fin = 1;
}
else{
fin = 0;
}
}
void f64(){ // 0 - '
if (((int)(flag[64])*(int)(flag[64]) + -87 * (int)(flag[64]) + 1872 ) || ((int)(flag[66])*(int)(flag[66]) + -87 * (int)(flag[66]) + 1872 )){
fin = 1;
}
else{
fin = 0;
}
}
void f65(){ // W - }
if (((int)(flag[65])*(int)(flag[65]) + -212 * (int)(flag[65]) + 10875 ) || ((int)(flag[67])*(int)(flag[67]) + -212 * (int)(flag[67]) + 10875 )){
fin = 1;
}
else{
fin = 0;
}
}
int main(int argc, char **argv)
{
klee_make_symbolic(flag, sizeof(flag), "flag");
const char format[] = "hackim18{''}";
for(i=0; i<10; ++i) klee_assume(flag[i] == format[i]);
klee_assume(flag[66] == '\'');
klee_assume(flag[67] == '}');
f0(); if(fin) return 1;
f1(); if(fin) return 1;
f2(); if(fin) return 1;
f3(); if(fin) return 1;
f4(); if(fin) return 1;
f5(); if(fin) return 1;
f6(); if(fin) return 1;
f7(); if(fin) return 1;
f8(); if(fin) return 1;
f9(); if(fin) return 1;
f10(); if(fin) return 1;
f11(); if(fin) return 1;
f12(); if(fin) return 1;
f13(); if(fin) return 1;
f14(); if(fin) return 1;
f15(); if(fin) return 1;
f16(); if(fin) return 1;
f17(); if(fin) return 1;
f18(); if(fin) return 1;
f19(); if(fin) return 1;
f20(); if(fin) return 1;
f21(); if(fin) return 1;
f22(); if(fin) return 1;
f23(); if(fin) return 1;
f24(); if(fin) return 1;
f25(); if(fin) return 1;
f26(); if(fin) return 1;
f27(); if(fin) return 1;
f28(); if(fin) return 1;
f29(); if(fin) return 1;
f30(); if(fin) return 1;
f31(); if(fin) return 1;
f32(); if(fin) return 1;
f33(); if(fin) return 1;
f34(); if(fin) return 1;
f35(); if(fin) return 1;
f36(); if(fin) return 1;
f37(); if(fin) return 1;
f38(); if(fin) return 1;
f39(); if(fin) return 1;
f40(); if(fin) return 1;
f41(); if(fin) return 1;
f42(); if(fin) return 1;
f43(); if(fin) return 1;
f44(); if(fin) return 1;
f45(); if(fin) return 1;
f46(); if(fin) return 1;
f47(); if(fin) return 1;
f48(); if(fin) return 1;
f49(); if(fin) return 1;
f50(); if(fin) return 1;
f51(); if(fin) return 1;
f52(); if(fin) return 1;
f53(); if(fin) return 1;
f54(); if(fin) return 1;
f55(); if(fin) return 1;
f56(); if(fin) return 1;
f57(); if(fin) return 1;
f58(); if(fin) return 1;
f59(); if(fin) return 1;
f60(); if(fin) return 1;
f61(); if(fin) return 1;
f62(); if(fin) return 1;
f63(); if(fin) return 1;
f64(); if(fin) return 1;
f65(); if(fin) return 1;
if(!fin) klee_assert(0);
return 0;
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment