code: def trim_core(self):
          
  
          for i in range(self.trim):
              # call solver with core assumption only
              # it must return 'unsatisfiable'
              self.oracle.solve(assumptions=self.core)
  
              # extract a new core
              new_core = self.oracle.get_core()
  
              if len(new_core) == len(self.core):
                  # stop if new core is not better than the previous one
                  break
  
              # otherwise, update core
              self.core = new_core
docs: This method trims a previously extracted unsatisfiable
              core at most a given number of times. If a fixed point is
              reached before that, the method returns.