code: def eval(
          self, expression: z3.ExprRef, model_completion: bool = False
      ) -> Union[None, z3.ExprRef]:
          
          for internal_model in self.raw:
              is_last_model = self.raw.index(internal_model) == len(self.raw) - 1
              is_relevant_model = expression.decl() in list(internal_model.decls())
              if is_relevant_model or is_last_model:
                  return internal_model.eval(expression, model_completion)
          return None
docs: Evaluate the expression using this model
  
          :param expression: The expression to evaluate
          :param model_completion: Use the default value if the model has no interpretation of the given expression
          :return: The evaluated expression