code: private void block() {
          final long steps = this.limits.simpSteps;
          assert this.level == 0;
          assert !this.config.plain;
          if (!this.config.block) { return; }
          if (this.config.blkwait >= this.stats.simplifications) { return; }
          assert this.simplifier == Simplifier.TOPSIMP;
          this.simplifier = Simplifier.BLOCK;
          updateCands();
          final long limit;
          if (this.stats.simplifications <= this.config.blkrtc) { limit = Long.MAX_VALUE; } else { limit = this.stats.steps + 10 * steps / sizePenalty(); }
          while (this.empty == null && !this.candsBlock.empty() && this.stats.steps++ < limit) {
              final int cand = this.candsBlock.top();
              final long priority = this.candsBlock.priority(cand);
              this.candsBlock.pop(cand);
              if (priority == 0 || !var(cand).free()) { continue; }
              blockLit(cand);
              blockLit(-cand);
          }
          assert this.schedule;
          this.schedule = false;
          assert this.simplifier == Simplifier.BLOCK;
          this.simplifier = Simplifier.TOPSIMP;
      }
docs: Blocked Clause Elimination.