code: def _compute(self, approx):
          
  
          i = 0
  
          while i < len(approx):
              to_test = approx[:i] + approx[(i + 1):]
              sel, clid = approx[i], self.vmap[approx[i]]
  
              if self.verbose > 1:
                  print('c testing clid: {0}'.format(clid), end='')
  
              if self.oracle.solve(assumptions=to_test):
                  if self.verbose > 1:
                      print(' -> sat (keeping {0})'.format(clid))
  
                  i += 1
              else:
                  if self.verbose > 1:
                      print(' -> unsat (removing {0})'.format(clid))
  
                  approx = to_test
docs: Deletion-based MUS extraction. Given an over-approximation of an
              MUS, i.e. an unsatisfiable core previously returned by a SAT
              oracle, the method represents a loop, which at each iteration
              removes a clause from the core and checks whether the remaining
              clauses of the approximation are unsatisfiable together with the
              hard clauses.
  
              Soft clauses are (de)activated using the standard MiniSat-like
              assumptions interface [2]_. Each soft clause :math:`c` is augmented
              with a selector literal :math:`s`, e.g. :math:`(c) \gets (c \\vee
              \\neg{s})`. As a result, clause :math:`c` can be activated by
              assuming literal :math:`s`. The over-approximation provided as an
              input is specified as a list of selector literals for clauses in
              the unsatisfiable core.
  
              .. [2] Niklas Eén, Niklas Sörensson. *Temporal induction by
                  incremental SAT solving*. Electr. Notes Theor. Comput. Sci.
                  89(4). 2003. pp. 543-560
  
              :param approx: an over-approximation of an MUS
              :type approx: list(int)
  
              Note that the method does not return. Instead, after its execution,
              the input over-approximation is refined and contains an MUS.