required: python3 z3-solver (pip install z3-solver)

to run: python3 any_file.py