docs: def enum_models(self, assumptions=[]):
          """
              Iterate over models of the internal formula.
          """
  
          if self.glucose:
              done = False
              while not done:
                  if self.use_timer:
                      start_time = time.clock()
  
                  self.status = pysolvers.glucose41_solve(self.glucose, assumptions)
  
                  if self.use_timer:
                      self.call_time = time.clock() - start_time
                      self.accu_time += self.call_time
  
                  model = self.get_model()
  
                  if model:
                      self.add_clause([-l for l in model])  # blocking model
                      yield model
                  else:
                      done = True