more deadcode eliminated

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

diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp
index 609f94430b6e6b0d12f59bfa6eac38a068ce8448..3b7c77dc14cf6b62a2f3555dbd9dd170eae0674b 100644 (file)
--- a/src/c_interface/c_interface.cpp
+++ b/src/c_interface/c_interface.cpp
@@ -27,7 +27,8 @@ typedef BEEV::CompleteCounterExample*    CompleteCEStar;
 BEEV::ASTVec *decls = NULL;
 //vector<BEEV::ASTNode *> created_exprs;
 
-// persist holds a copy of ASTNodes so that the reference count of objects we have pointers to doesn't hit zero.
+// persist holds a copy of ASTNodes so that the reference count of
+// objects we have pointers to doesn't hit zero.
 vector<BEEV::ASTNode*> persist;
 bool cinterface_exprdelete_on_flag = false;
 

diff --git a/src/to-sat/ToSAT.h b/src/to-sat/ToSAT.h
index 222235e5fa2b8cba19157a488d63ffcbcb975ae4..4654ae6427b1e9d2bd9f9fcfd082b3e26338da6d 100644 (file)
--- a/src/to-sat/ToSAT.h
+++ b/src/to-sat/ToSAT.h
@@ -114,11 +114,6 @@ namespace BEEV
     bool toSATandSolve(MINISAT::Solver& S,
                       ClauseList& cll, bool add_xor_clauses=false);
     
-    // Calls SAT simplifier, array transformer (abstraction
-    // refinement), bitvector solver, and SAT solver. Returns the
-    // answer to the input query
-    SOLVER_RETURN_TYPE TopLevelSATAux(const ASTNode& query);
-
     //print the STP solver output
     void PrintOutput(SOLVER_RETURN_TYPE ret);