code: def minimize_core(self):
          
  
          if self.minz and len(self.core) > 1:
              self.core = sorted(self.core, key=lambda l: self.wght[l])
              self.oracle.conf_budget(1000)
  
              i = 0
              while i < len(self.core):
                  to_test = self.core[:i] + self.core[(i + 1):]
  
                  if self.oracle.solve_limited(assumptions=to_test) == False:
                      self.core = to_test
                  else:
                      i += 1
docs: Reduce a previously extracted core and compute an
              over-approximation of an MUS. This is done using the
              simple deletion-based MUS extraction algorithm.
  
              The idea is to try to deactivate soft clauses of the
              unsatisfiable core one by one while checking if the
              remaining soft clauses together with the hard part of the
              formula are unsatisfiable. Clauses that are necessary for
              preserving unsatisfiability comprise an MUS of the input
              formula (it is contained in the given unsatisfiable core)
              and are reported as a result of the procedure.
  
              During this core minimization procedure, all SAT calls are
              dropped after obtaining 1000 conflicts.