Reworked z3_problems.py to match sample_problems.py