From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Thu, 12 May 2011 04:56:59 +0000 (+0000)
Subject: Improvement. Make error checking more normal.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=36cbdc860081b5cd3efde4e8275a0d184609a591;p=francis%2Fstp.git

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 4b8b702..60d08c2 100644
--- 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 63b9659..2eabd58 100644
--- 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);
             }