From: vijay_ganesh <vijay_ganesh@e59a4935-1847-0410-ae03-e826735625c1>
Date: Fri, 13 Nov 2009 18:41:12 +0000 (+0000)
Subject: more deadcode eliminated
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=956cdf0923c5fc648feabe845307be286d1c661b;p=francis%2Fstp.git

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 609f944..3b7c77d 100644
--- 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 222235e..4654ae6 100644
--- 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);