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