code: private void distill() {
          final long steps = this.limits.simpSteps;
          assert this.level == 0;
          assert !this.config.plain;
          if (!this.config.distill) { return; }
          final long limit = this.stats.steps + steps / sizePenalty();
          boolean changed = false;
          boolean done = this.clauses.empty();
          if (this.distilled >= this.clauses.size()) { this.distilled = 0; }
          while (this.empty == null && !done && this.stats.steps++ < limit) {
              final CLClause c = this.clauses.get(this.distilled);
              if (!c.redundant() && !c.dumped() && c.large() && !satisfied(c)) {
                  CLClause conflict = null;
                  assert this.ignore == null;
                  this.ignore = c;
                  int lit;
                  for (int p = 0; conflict == null && p < c.lits().size(); p++) {
                      lit = c.lits().get(p);
                      final byte v = val(lit);
                      if (v == VALUE_FALSE) { continue; }
                      if (v == VALUE_TRUE) {
                          this.stats.distillStrengthened++;
                          strengthen(c, lit);
                          changed = true;
                          break;
                      }
                      assume(-lit);
                      conflict = bcp();
                  }
                  this.ignore = null;
                  if (conflict != null) {
                      analyze(conflict);
  
                      if (this.level == 0) {
                          assert this.next < this.trail.size();
                          this.stats.distillUnits++;
                          changed = true;
                          conflict = bcp();
                          if (conflict != null) {
                              analyze(conflict);
                              assert this.empty != null;
                          }
                      } else {
                          this.stats.distillSubsumed++;
                          dumpClause(c);
                      }
                  }
                  backtrack();
              }
              if (++this.distilled == this.clauses.size()) {
                  if (changed) { changed = false; } else { done = true; }
                  this.distilled = 0;
              }
          }
      }
docs: Distills units and subsumes/strengthens clauses.