vprover / vampire

The Vampire Theorem Prover
https://vprover.github.io/
Other
302 stars 52 forks source link

CASC changes #568

Closed MichaelRawson closed 5 months ago

MichaelRawson commented 5 months ago

We made some last-minute changes for CASC, as usual. Let's put these here for general inspection and choose what to merge eventually.

quickbeam123 commented 5 months ago

-fibus and -fsoe, while being used in the UEQ schedule are candidates for immediate kick-out. So _skipNonequational in UnitClauseLiteralIndex::handleClause or forwardIbuSubsumed in Statistics might not need any polishing.