Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- 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) {
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement