Scripts and code for HackOvert Z3 function modeling

challenge.c

// Challenge from:
// https://www.reddit.com/r/ExploitDev/comments/gv72xr/reverse_engineer_passphrase_check/

#include <stdio.h>
#include <string.h>

int check(char* input) {
    if (strlen(input) != 15) {
        return 0;
    } else {
        int a = input[0];
        int b = input[1];
        int c = input[2];
        int d = input[3];
        int e = input[4];
        int f = input[5];
        int g = input[6];
        int h = input[7];
        int i = input[8];
        int j = input[9];
        int k = input[10];
        int l = input[11];
        int m = input[12];
        int n = input[13];
        int o = input[14];

        if (5 != (j + h) / (k ^ a)) {
            return 0;
        }
        if (106 != ((o % e) ^ f) + a) {
            return 0;
        }
        if (90 != (b - (c ^ d)) % l) {
            return 0;
        }
        if (19 != (f ^ b) - (c / n)) {
            return 0;
        }
        if (112 != ((o / l) % k) + n) {
            return 0;
        }
        if (1 != ((b / c) & (g ^ n))) {
            return 0;
        }
        if (27 != (((m - d) + g) ^ h)) {
            return 0;
        }
        if ('Q' != (((e / l) * d) & f)) {
            return 0;
        }
        if (66 != (j % h) + (m - g)) {
            return 0;
        }
        if (5 != ((h % i) >> (k - e))) {
            return 0;
        }
        if (83 != ((o & f) / h) * d) {
            return 0;
        }
        if (' ' != (((c - g) - a) & m)) {
            return 0;
        }
        if (26 != (((m / a) ^ g) ^ f)) {
            return 0;
        }
        if (17 != (o ^ j) - (h - d)) {
            return 0;
        }
        if (16 != ((d % i) & (h - j))) {
            return 0;
        }
        if (16 != (i - (a & k)) % h) {
            return 0;
        }
        if (112 != ((l * k) + f) / g) {
            return 0;
        }
        if (19 != ((f ^ m) ^ (b - h))) {
            return 0;
        }
        if (43 != (d * o) / (g + b)) {
            return 0;
        }
        if (2 != (((a + k) * i) & l)) {
            return 0;
        }
        if (1 != (m + c) / (a + j)) {
            return 0;
        }
        if (17 != ((f - m) % k) % e) {
            return 0;
        }
        if ('>' != (((f / g) + a) ^ o)) {
            return 0;
        }
        return 1;
    }
}

int main(int argc, char **argv) {
    int result = 0;

    if (argc < 2) {
        printf("Usage: %s <input>\n", argv[0]);
        return 1;
    }
    
    if (check(argv[1])) {
        puts("Yes! You found the correct input!\n");
    } else {
        puts("Sorry, that input is wrong. :(\n");
    }

    return 0;
}

challenge.txt

Challenge from:
https://www.reddit.com/r/ExploitDev/comments/gv72xr/reverse_engineer_passphrase_check/

Reverse Engineer passphrase check
I got this piece of code to reverse that only matches one specific string input.

public static boolean check(String input) {
    if (input.length() != 15) {
        return false;
    } else {
        int a = input.charAt(0);
        int b = input.charAt(1);
        int c = input.charAt(2);
        int d = input.charAt(3);
        int e = input.charAt(4);
        int f = input.charAt(5);
        int g = input.charAt(6);
        int h = input.charAt(7);
        int i = input.charAt(8);
        int j = input.charAt(9);
        int k = input.charAt(10);
        int l = input.charAt(11);
        int m = input.charAt(12);
        int n = input.charAt(13);
        int o = input.charAt(14);

        if (5 != (j + h) / (k ^ a)) {
            return false;
        }
        if (106 != ((o % e) ^ f) + a) {
            return false;
        }
        if (90 != (b - (c ^ d)) % l) {
            return false;
        }
        if (19 != (f ^ b) - (c / n)) {
            return false;
        }
        if (112 != ((o / l) % k) + n) {
            return false;
        }
        if (1 != ((b / c) & (g ^ n))) {
            return false;
        }
        if (27 != (((m - d) + g) ^ h)) {
            return false;
        }
        if ('Q' != (((e / l) * d) & f)) {
            return false;
        }
        if (66 != (j % h) + (m - g)) {
            return false;
        }
        if (5 != ((h % i) >> (k - e))) {
            return false;
        }
        if (83 != ((o & f) / h) * d) {
            return false;
        }
        if (' ' != (((c - g) - a) & m)) {
            return false;
        }
        if (26 != (((m / a) ^ g) ^ f)) {
            return false;
        }
        if (17 != (o ^ j) - (h - d)) {
            return false;
        }
        if (16 != ((d % i) & (h - j))) {
            return false;
        }
        if (16 != (i - (a & k)) % h) {
            return false;
        }
        if (112 != ((l * k) + f) / g) {
            return false;
        }
        if (19 != ((f ^ m) ^ (b - h))) {
            return false;
        }
        if (43 != (d * o) / (g + b)) {
            return false;
        }
        if (2 != (((a + k) * i) & l)) {
            return false;
        }
        if (1 != (m + c) / (a + j)) {
            return false;
        }
        if (17 != ((f - m) % k) % e) {
            return false;
        }
        if ('>' != (((f / g) + a) ^ o)) {
            return false;
        }
        return true;
    }
}

solve.py

import z3

a = z3.BitVec('a', 32)
b = z3.BitVec('b', 32)
c = z3.BitVec('c', 32)
d = z3.BitVec('d', 32)
e = z3.BitVec('e', 32)
f = z3.BitVec('f', 32)
g = z3.BitVec('g', 32)
h = z3.BitVec('h', 32)
i = z3.BitVec('i', 32)
j = z3.BitVec('j', 32)
k = z3.BitVec('k', 32)
l = z3.BitVec('l', 32)
m = z3.BitVec('m', 32)
n = z3.BitVec('n', 32)
o = z3.BitVec('o', 32)

s = z3.Solver()

# implied constraints due to type `String` on input
s.add(z3.And(a >= 32, a <= 126))
s.add(z3.And(b >= 32, b <= 126))
s.add(z3.And(c >= 32, c <= 126))
s.add(z3.And(d >= 32, d <= 126))
s.add(z3.And(e >= 32, e <= 126))
s.add(z3.And(f >= 32, f <= 126))
s.add(z3.And(g >= 32, g <= 126))
s.add(z3.And(h >= 32, h <= 126))
s.add(z3.And(i >= 32, i <= 126))
s.add(z3.And(j >= 32, j <= 126))
s.add(z3.And(k >= 32, k <= 126))
s.add(z3.And(l >= 32, l <= 126))
s.add(z3.And(m >= 32, m <= 126))
s.add(z3.And(n >= 32, n <= 126))
s.add(z3.And(o >= 32, o <= 126))

# constraints from C
# predicate logic inverted to avoid `false`
# return in check()
s.add(5 == (j + h) / (k ^ a))
s.add(106 == ((o % e) ^ f) + a)
s.add(90 == (b - (c ^ d)) % l)
s.add(19 == (f ^ b) - (c / n))
s.add(112 == ((o / l) % k) + n)
s.add(1 == ((b / c) & (g ^ n)))
s.add(27 == (((m - d) + g) ^ h))
s.add(81 == (((e / l) * d) & f))
s.add(66 == (j % h) + (m - g))
s.add(5 == ((h % i) >> (k - e)))
s.add(83 == ((o & f) / h) * d)
s.add(32 == (((c - g) - a) & m))
s.add(26 == (((m / a) ^ g) ^ f))
s.add(17 == (o ^ j) - (h - d))
s.add(16 == ((d % i) & (h - j)))
s.add(16 == (i - (a & k)) % h)
s.add(112 == ((l * k) + f) / g)
s.add(19 == ((f ^ m) ^ (b - h)))
s.add(43 == (d * o) / (g + b))
s.add(2 == (((a + k) * i) & l))
s.add(1 == (m + c) / (a + j))
s.add(17 == ((f - m) % k) % e)
s.add(62 == (((f / g) + a) ^ o))

if s.check().r == 1:
    model = s.model()
    print(model)
    solution = ""
    solution += chr(model[a].as_long())
    solution += chr(model[b].as_long())
    solution += chr(model[c].as_long())
    solution += chr(model[d].as_long())
    solution += chr(model[e].as_long())
    solution += chr(model[f].as_long())
    solution += chr(model[g].as_long())
    solution += chr(model[h].as_long())
    solution += chr(model[i].as_long())
    solution += chr(model[j].as_long())
    solution += chr(model[k].as_long())
    solution += chr(model[l].as_long())
    solution += chr(model[m].as_long())
    solution += chr(model[n].as_long())
    solution += chr(model[o].as_long())
    print("Solution: ({})".format(solution))
else:
    print("unsat")