temp.cpp

    for (int k = 1;; ++k) {
      if (st.m.verbosity() > Options::Informative) cout << "Level " << k << endl;
      extend(st, k);
      bool trivial = strengthen(st, k);
      auto rat = st.m.attachment<RchAttachment>(Key::RCH);
      rat->updateCexLowerBound(k + 2, string(st.ss.reverse ? "IC3r" : "IC3"));
      st.m.release(rat);
      propagateClauses(st, k, trivial, shortCircuit);
      renewSAT(st);
    }


--------------------------------------------------------------------------------


            throw CEX(st.cex, toK, indCubes);
          }
          else {
            throw CEX(st.cex, toK);
          }

--------------------------------------------------------------------------------

    try {
      check(sstate, !proofCNF);
    }
    catch (CEX const & cex) {