Commit 0f594b78 by Alan Mishchenko

Commented out the default call to UNSAT core verification.

parent 9726d5a8
...@@ -1037,7 +1037,7 @@ p->timeTotal += clock() - clkTotal; ...@@ -1037,7 +1037,7 @@ p->timeTotal += clock() - clkTotal;
if ( fVerbose ) if ( fVerbose )
printf( "Root clauses = %d. Learned clauses = %d. UNSAT core size = %d.\n", printf( "Root clauses = %d. Learned clauses = %d. UNSAT core size = %d.\n",
p->pCnf->nRoots, p->pCnf->nClauses-p->pCnf->nRoots, Vec_IntSize(vCore) ); p->pCnf->nRoots, p->pCnf->nClauses-p->pCnf->nRoots, Vec_IntSize(vCore) );
Intp_ManUnsatCoreVerify( p->pCnf, vCore ); // Intp_ManUnsatCoreVerify( p->pCnf, vCore );
return vCore; return vCore;
} }
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment