# Tough
This is a simple java program:
```javaimport java.util.*;
public class tough{    public static int[] realflag = {9,4,23,8,17,1,18,0,13,7,2,20,16,10,22,12,19,6,15,21,3,14,5,11};    public static int[] therealflag = {20,16,12,9,6,15,21,3,18,0,13,7,1,4,23,8,17,2,10,22,19,11,14,5};    public static HashMap<Integer, Character> theflags = new HashMap<>();    public static HashMap<Integer, Character> theflags0 = new HashMap<>();    public static HashMap<Integer, Character> theflags1 = new HashMap<>();    public static HashMap<Integer, Character> theflags2 = new HashMap<>();    public static boolean m = true;    public static boolean g = false;     public static void main(String args[]) {        Scanner scanner = new Scanner(System.in);        System.out.print("Enter flag: ");        String userInput = scanner.next();        String input = userInput.substring("rtcp{".length(),userInput.length()-1);        if (check(input)) {            System.out.println("Access granted.");        } else {            System.out.println("Access denied!");        }    }     public static boolean check(String input){        boolean h = false;        String flag = "ow0_wh4t_4_h4ckr_y0u_4r3";        // realflag        createMap(theflags, input, m);        // therealflag        createMap(theflags0, flag, g);        // therealflag        createMap(theflags1, input, g);        // realflag        createMap(theflags2, flag, m);        String theflag = "";        String thefinalflag = "";        int i = 0;        System.out.println(input.length());        System.out.println(flag.length());        if(input.length() != flag.length()){            return h;        }        if(input.charAt(input.length()-2) != 'o'){            return false;        }        if(!input.substring(2,4).equals("r3") || input.charAt(5) != '_' || input.charAt(7) != '_'){            return false;        }        System.out.println("arrived here");        //rtcp{h3r3s_a_fr33_fl4g!}        for(; i < input.length()-3; i++){            theflag += theflags.get(i);        }        for(; i < input.length();i++){            theflag += theflags1.get(i);        }        for(int p = 0; p < theflag.length(); p++){            thefinalflag += (char)((int)(theflags0.get(p)) + (int)(theflag.charAt(p)));        }        for(int p = 0; p < theflag.length(); p++){            if((int)(thefinalflag.charAt(p)) > 146 && (int)(thefinalflag.charAt(p)) < 157){                // thefinalflag = thefinalflag[0:p] + chr(thefinalflag[p] + 10) + thefinalflag[p+1:]                // thefinalflag[p] = thefinalflag[p] + 10                thefinalflag = thefinalflag.substring(0,p) + (char)((int)(thefinalflag.charAt(p)+10)) + thefinalflag.substring(p+1);            }        }        return thefinalflag.equals("ì¨ ¢«¢¥Ç©© ÂëÏãÒËãhÔÊ");    }    public static void createMap(HashMap owo, String input, boolean uwu){        if(uwu){            for(int i = 0; i < input.length(); i++){                owo.put(realflag[i], input.charAt(i));            }        } else{            for(int i = 0; i < input.length(); i++){                owo.put(therealflag[i], input.charAt(i));            }        }    }}```
 We can crack it using z3:
```py#!/usr/bin/env python3
from z3 import *import sys
s = Solver()realflag = [9,4,23,8,17,1,18,0,13,7,2,20,16,10,22,12,19,6,15,21,3,14,5,11]therealflag = [20,16,12,9,6,15,21,3,18,0,13,7,1,4,23,8,17,2,10,22,19,11,14,5]flag = "ow0_wh4t_4_h4ckr_y0u_4r3"my_input = [BitVec(f"a_{i:2}", 8) for i in range(len(flag))]theflag = [BitVec(f"c_{i}", 8) for i in range(len(flag) * 2)]thefinalflag = [BitVec(f"f_{i}", 8) for i in range(len(flag) * 2)]definitive = [BitVec(f"s_{i}", 8) for i in range(len(flag) * 2)]
theflags = {}theflags0 = {}theflags1 = {}theflags2 = {}for i in range(len(my_input)):    theflags[realflag[i]] = my_input[i]    theflags0[therealflag[i]] = flag[i]    theflags1[therealflag[i]] = my_input[i]    theflags2[realflag[i]] = flag[i]
for m in my_input:    s.add(m >= 0x20, m < 0x7f)
s.add(my_input[-2] == ord('o'))for i in range(2):    s.add(my_input[i + 2] != ord("re"[i]))s.add(my_input[5] == ord('_'))s.add(my_input[7] == ord('_'))
k = 0z = 0for i in range(len(my_input) - 3):    s.add(theflag[k] == theflags.get(i))    k += 1
for i in range(len(my_input) - 3, len(my_input)):    s.add(theflag[k] == theflags1.get(i))    k += 1
for i in range(k):    s.add(thefinalflag[z] == ord(theflags0.get(i)) + theflag[i])    z += 1
# x == 5# x == x + 5for i in range(k):    x = If(And(thefinalflag[i] > 146, thefinalflag[i] < 157), 10, 0)    s.add(definitive[i] == thefinalflag[i] + Int2BV(x, 8))
final_check = [157, 157, 236, 168, 160, 162, 171, 162, 165, 199, 169, 169, 160, 194, 235, 207, 227, 210, 157, 203, 227, 104, 212, 202]for f, c in zip(definitive, final_check):    s.add(f == c)
print(s.check())m = s.model()#print(m)model = sorted([(d, m[d]) for d in m], key = lambda x: str(x[0]))for m in model:    if "a" in str(m[0]):        print(chr(m[1].as_long()), end='')print()```
Flag:
rtcp{h3r3s_4_c0stly_fl4g_4you}