Improvement. Make error checking more normal.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1335 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/src/to-sat/AIG/ToCNFAIG.cpp b/src/to-sat/AIG/ToCNFAIG.cpp
index 4b8b702aa55d02c4f8d3820bd7db37a7efb4797a..60d08c2168f3a29ad950deb3b8b7e2597fb4ac76 100644 (file)
--- a/src/to-sat/AIG/ToCNFAIG.cpp
+++ b/src/to-sat/AIG/ToCNFAIG.cpp
@@ -67,7 +67,7 @@ void ToCNFAIG::toCNF(const BBNodeAIG& top, Cnf_Dat_t*& cnfData,
        if (uf.stats_flag)
                cerr << "Nodes before AIG rewrite:" << nodeCount << endl;
 
-       if (!needAbsRef && uf.isSet("aig_rewrite","0")) {
+       if (!needAbsRef && uf.isSet("aig-rewrite","0")) {
                Dar_LibStart();
                Aig_Man_t * pTemp;
                Dar_RwrPar_t Pars, *pPars = &Pars;

diff --git a/src/to-sat/AIG/ToSATAIG.cpp b/src/to-sat/AIG/ToSATAIG.cpp
index 63b9659347a534a9a2b6c6a9c4bd9fcdc45a14d4..2eabd588364163e54fee6c7463d771de68437b78 100644 (file)
--- a/src/to-sat/AIG/ToSATAIG.cpp
+++ b/src/to-sat/AIG/ToSATAIG.cpp
@@ -101,12 +101,7 @@ namespace BEEV
               + 1]; pLit < pStop; pLit++)
             {
               SATSolver::Var var = (*pLit) >> 1;
-              if (!(var < satSolver.nVars()))
-              {
-                 cerr << var << " ";
-                 cerr << satSolver.nVars();
-                 exit(1);
-              }
+              assert ((var < satSolver.nVars()));
               Minisat::Lit l = SATSolver::mkLit(var, (*pLit) & 1);
               satSolverClause.push(l);
             }