diff --git a/2021/d24/ex1/ex1.py b/2021/d24/ex1/ex1.py
index 5d703d8..05e7aac 100755
--- a/2021/d24/ex1/ex1.py
+++ b/2021/d24/ex1/ex1.py
@@ -92,12 +92,13 @@ def solve(input: List[str]) -> int:
 
         solver.add(registers["z"] == zero)
 
-        model_number = functools.reduce(lambda a, b: a * 10 + b, digits)
+        digits_to_num = lambda digits: functools.reduce(lambda a, b: a * 10 + b, digits)
 
-        solver.maximize(model_number)
+        solver.maximize(digits_to_num(digits))
         assert solver.check() == z3.sat  # Sanity check
 
-        return solver.model().eval(model_number)
+        model = solver.model()
+        return digits_to_num(model[d].as_long() for d in digits)
 
     return run_z3(parse())
 
diff --git a/2021/d24/ex2/ex2.py b/2021/d24/ex2/ex2.py
index 63231dd..8a9b09a 100755
--- a/2021/d24/ex2/ex2.py
+++ b/2021/d24/ex2/ex2.py
@@ -92,12 +92,13 @@ def solve(input: List[str]) -> int:
 
         solver.add(registers["z"] == zero)
 
-        model_number = functools.reduce(lambda a, b: a * 10 + b, digits)
+        digits_to_num = lambda digits: functools.reduce(lambda a, b: a * 10 + b, digits)
 
-        solver.minimize(model_number)
+        solver.minimize(digits_to_num(digits))
         assert solver.check() == z3.sat  # Sanity check
 
-        return solver.model().eval(model_number)
+        model = solver.model()
+        return digits_to_num(model[d].as_long() for d in digits)
 
     return run_z3(parse())