Idk what tf i was doing at 4am

rsa.py

# import random
import math
from z3 import *

prime = 7919*7583

def isPrime(x):
    y, z = Ints("y z")
    return And(x > 1, Not(Exists([y, z], And(y < x, z < x, y > 1, z > 1, x == y*z))))

def guesser(n):
    s = Solver()

# Define the variables for the program
    num = Int('num')

    # Add constraints to the solver
    s.add(num < n)  # the number should be greater than 1
    s.add(Not(isPrime(num)))  # the number should not be a prime number
    s.add(num > 1)
    print(int(math.sqrt(n)) + 1)
    for i in range(2, int(math.sqrt(n)) + 1):
        if n % i == 0:
            print(i)
            s.add(num % i != 0)
    # Check if the constraints are satisfiable
    if s.check() == sat:
        # Print the satisfying solution
        return s.model()[num].as_long()
    else:
        exit(1)

def phase_estimator(a, n):
    r = 0
    while True:
        print(a, r)
        exp = a ** r 
        if exp > n:
            res = exp % n
            if res == 1:
                break
            else:
                r += 1
        else:
            r += 1

    return a, r
    

def main():

    a = guesser(prime)
    base, exp = phase_estimator(a, prime)

    f1 = math.gcd(( base ** (exp//2) + 1 ), prime)
    f2 = math.gcd((base ** (exp//2) - 1), prime) 

    print(f1, f2)
    
if __name__ == "__main__":
  main()