Forgot to remove the actual stp directory.

git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@161056 91177308-0d34-0410-b5e6-96231b3b80d8

15 files changed, 0 insertions, 7571 deletions

diff --git a/stp/AST/AST.cpp b/stp/AST/AST.cpp
deleted file mode 100644
index 63319de9..00000000
--- a/stp/AST/AST.cpp
+++ /dev/null
@@ -1,1579 +0,0 @@
-/********************************************************************
- * AUTHORS: Vijay Ganesh, David L. Dill
- *
- * BEGIN DATE: November, 2005
- *
- * LICENSE: Please view LICENSE file in the home dir of this Program
- ********************************************************************/
-// -*- c++ -*-
-
-#include "AST.h"
-namespace BEEV {
-  //some global variables that are set through commandline options. it
-  //is best that these variables remain global. Default values set
-  //here
-  //
-  //collect statistics on certain functions
-  bool stats = false;
-  //print DAG nodes
-  bool print_nodes = false;
-  //tentative global var to allow for variable activity optimization
-  //in the SAT solver. deprecated.
-  bool variable_activity_optimize = false;
-  //run STP in optimized mode
-  bool optimize = true;
-  //do sat refinement, i.e. underconstraint the problem, and feed to
-  //SAT. if this works, great. else, add a set of suitable constraints
-  //to re-constraint the problem correctly, and call SAT again, until
-  //all constraints have been added.
-  bool arrayread_refinement = true;
-  //flag to control write refinement
-  bool arraywrite_refinement = true;
-  //check the counterexample against the original input to STP
-  bool check_counterexample = false;
-  //construct the counterexample in terms of original variable based
-  //on the counterexample returned by SAT solver
-  bool construct_counterexample = true;
-  bool print_counterexample = false;
-  //if this option is true then print the way dawson wants using a
-  //different printer. do not use this printer.
-  bool print_arrayval_declaredorder = false;
-  //flag to decide whether to print "valid/invalid" or not
-  bool print_output = false;
-  //do linear search in the array values of an input array. experimental
-  bool linear_search = false;
-  //print the variable order chosen by the sat solver while it is
-  //solving.
-  bool print_sat_varorder = false; 
-  //turn on word level bitvector solver
-  bool wordlevel_solve = true;
-  //turn off XOR flattening
-  bool xor_flatten = false;
-
-  //the smtlib parser has been turned on
-  bool smtlib_parser_enable = false;
-  //print the input back
-  bool print_STPinput_back = false;
-  
-  //global BEEVMGR for the parser
-  BeevMgr * globalBeevMgr_for_parser;
-
-  void (*vc_error_hdlr)(const char* err_msg) = NULL;
-  /** This is reusable empty vector, for representing empty children arrays */
-  ASTVec _empty_ASTVec;  
-  ////////////////////////////////////////////////////////////////
-  //  ASTInternal members
-  ////////////////////////////////////////////////////////////////  
-  /** Trivial but virtual destructor */
-  ASTInternal::~ASTInternal() { }
-
-  ////////////////////////////////////////////////////////////////
-  //  ASTInterior members
-  ////////////////////////////////////////////////////////////////
-  /** Copy constructor */
-  // ASTInterior::ASTInterior(const ASTInterior &int_node)
-  // {
-  //   _kind = int_node._kind;
-  //   _children = int_node._children;
-  // }
-  
-  /** Trivial but virtual destructor */
-  ASTInterior::~ASTInterior() { }
-  
-  // FIXME: Darn it! I think this ends up copying the children twice!
-  /** Either return an old node or create it if it doesn't exist. 
-      Note that nodes are physically allocated in the hash table. */
-  
-  // There is  an inelegance here that  I don't know how  to solve.  I'd
-  // like to heap allocate and do some other initialization on keys only
-  // if  they aren't  in  the hash  table.   It would  be  great if  the
-  // "insert"  method took a  "creator" class  so that  I could  do that
-  // between  when it  notices that  the key  is not  there and  when it
-  // inserts it.  Alternatively, it would be great if I could insert the
-  // temporary key and replace it  if it actually got inserted.  But STL
-  // hash_set  doesn't have  the creator  feature  and paternalistically
-  // declares that keys are immutable, even though (it seems to me) that
-  // they  could be  mutated if  the hash  value and  eq values  did not
-  // change.
-  
-  ASTInterior *BeevMgr::LookupOrCreateInterior(ASTInterior *n_ptr) {
-    ASTInteriorSet::iterator it;
-    
-    if ((it = _interior_unique_table.find(n_ptr)) == _interior_unique_table.end()) {
-      // Make a new ASTInterior node
-      // We want (NOT alpha) always to have alpha.nodenum + 1.
-      if (n_ptr->GetKind() == NOT) {
-	n_ptr->SetNodeNum(n_ptr->GetChildren()[0].GetNodeNum()+1);
-      }
-      else {
-	n_ptr->SetNodeNum(NewNodeNum());
-      }
-      pair<ASTInteriorSet::const_iterator, bool> p = _interior_unique_table.insert(n_ptr);
-      return *(p.first);
-    }
-    else
-      // Delete the temporary node, and return the found node.
-      delete n_ptr;
-      return *it;
-  }
-  
-  size_t ASTInterior::ASTInteriorHasher::operator() (const ASTInterior *int_node_ptr) const {
-    //size_t hashval = 0;
-    size_t hashval = ((size_t) int_node_ptr->GetKind());
-    const ASTVec &ch = int_node_ptr->GetChildren();
-    ASTVec::const_iterator iend = ch.end();
-    for (ASTVec::const_iterator i = ch.begin(); i != iend; i++) {
-      //Using "One at a time hash" by Bob Jenkins
-      hashval += i->Hash();
-      hashval += (hashval << 10);
-      hashval ^= (hashval >> 6);
-    }
-
-    hashval += (hashval << 3);
-    hashval ^= (hashval >> 11);
-    hashval += (hashval << 15);
-    return hashval;
-    //return hashval += ((size_t) int_node_ptr->GetKind());
-  }
-  
-
-  void ASTInterior::CleanUp() {
-    // cout << "Deleting node " << this->GetNodeNum() << endl;
-    _bm._interior_unique_table.erase(this);
-    delete this;
-  }
-
-  ////////////////////////////////////////////////////////////////
-  //  ASTNode members
-  ////////////////////////////////////////////////////////////////
-  //ASTNode constructors are inlined in AST.h
-  bool ASTNode::IsAlreadyPrinted() const {
-    BeevMgr &bm = GetBeevMgr();
-    return (bm.AlreadyPrintedSet.find(*this) != bm.AlreadyPrintedSet.end());
-  }
-
-  void ASTNode::MarkAlreadyPrinted() const {
-    // FIXME: Fetching BeevMgr is annoying.  Can we put this in lispprinter class?
-    BeevMgr &bm = GetBeevMgr();
-    bm.AlreadyPrintedSet.insert(*this);
-  }
-
-  // Get the name from a symbol (char *).  It's an error if kind != SYMBOL
-  const char *ASTNode::GetName() const {
-    if (GetKind() != SYMBOL)
-      FatalError("GetName: Called GetName on a non-symbol: ", *this);
-    return ((ASTSymbol *) _int_node_ptr)->GetName();    
-  }
-  
-  // Print in lisp format
-  ostream &ASTNode::LispPrint(ostream &os, int indentation) const {
-    // Clear the PrintMap
-    BeevMgr& bm = GetBeevMgr(); 
-    bm.AlreadyPrintedSet.clear();
-    return LispPrint_indent(os, indentation);
-  }
-
-  // Print newline and indentation, then print the thing.
-  ostream &ASTNode::LispPrint_indent(ostream &os,
-				     int indentation) const
-  {
-    os << endl << spaces(indentation);
-    LispPrint1(os, indentation);
-    return os;
-  }
-  
-  /** Internal function to print in lisp format.  Assume newline
-      and indentation printed already before first line.  Recursive
-      calls will have newline & indent, though */
-  ostream &ASTNode::LispPrint1(ostream &os, int indentation) const {
-    if (!IsDefined()) {
-      os << "<undefined>";
-      return os;
-    }
-    Kind kind = GetKind();
-    // FIXME: figure out how to avoid symbols with same names as kinds.
-//    if (kind == READ) {
-//      const ASTVec &children = GetChildren();
-//      children[0].LispPrint1(os, indentation);
-//	os << "[" << children[1] << "]";
-//    } else 
-    if(kind == BVGETBIT) {
-      const ASTVec &children = GetChildren();
-      // child 0 is a symbol.  Print without the NodeNum.
-      os << GetNodeNum() << ":";
-
-
-
-      children[0]._int_node_ptr->nodeprint(os);
-      //os << "{" << children[1].GetBVConst() << "}";
-      os << "{";
-      children[1]._int_node_ptr->nodeprint(os);
-      os << "}";
-    } else if (kind == NOT) {
-      const ASTVec &children = GetChildren();
-      os << GetNodeNum() << ":";	
-      os << "(NOT ";
-      children[0].LispPrint1(os, indentation);
-      os << ")";
-    }
-    else if (Degree() == 0) {
-      // Symbol or a kind with no children print as index:NAME if shared,
-      // even if they have been printed before.	
-      os << GetNodeNum() << ":";
-      _int_node_ptr->nodeprint(os); 
-      // os << "(" << _int_node_ptr->_ref_count << ")";
-      // os << "{" << GetValueWidth() << "}";
-    }
-    else if (IsAlreadyPrinted()) {
-      // print non-symbols as "[index]" if seen before.
-      os << "[" << GetNodeNum() << "]";
-      //	   << "(" << _int_node_ptr->_ref_count << ")";
-    }
-    else {
-      MarkAlreadyPrinted();
-      const ASTVec &children = GetChildren();
-      os << GetNodeNum() << ":"
-	//<< "(" << _int_node_ptr->_ref_count << ")" 
-	 << "(" << kind << " ";
-      // os << "{" << GetValueWidth() << "}";
-      ASTVec::const_iterator iend = children.end();
-      for (ASTVec::const_iterator i = children.begin(); i != iend; i++) {
-	i->LispPrint_indent(os, indentation+2);
-	}
-      os << ")";	
-    }
-    return os;
-  }
-
-  //print in PRESENTATION LANGUAGE
-  //
-  //two pass algorithm: 
-  //
-  //1. In the first pass, letize this Node, N: i.e. if a node
-  //1. appears more than once in N, then record this fact.
-  //
-  //2. In the second pass print a "global let" and then print N
-  //2. as follows: Every occurence of a node occuring more than
-  //2. once is replaced with the corresponding let variable.
-  ostream& ASTNode::PL_Print(ostream &os,
-			     int indentation) const {
-    // Clear the PrintMap
-    BeevMgr& bm = GetBeevMgr(); 
-    bm.PLPrintNodeSet.clear();
-    bm.NodeLetVarMap.clear();
-    bm.NodeLetVarVec.clear();
-    bm.NodeLetVarMap1.clear();
-
-    //pass 1: letize the node
-    LetizeNode();
-
-    //pass 2: 
-    //
-    //2. print all the let variables and their counterpart expressions
-    //2. as follows (LET var1 = expr1, var2 = expr2, ...
-    //
-    //3. Then print the Node itself, replacing every occurence of
-    //3. expr1 with var1, expr2 with var2, ...
-    //os << "(";
-    if(0 < bm.NodeLetVarMap.size()) {
-      //ASTNodeMap::iterator it=bm.NodeLetVarMap.begin();
-      //ASTNodeMap::iterator itend=bm.NodeLetVarMap.end();
-      std::vector<pair<ASTNode,ASTNode> >::iterator it = bm.NodeLetVarVec.begin();
-      std::vector<pair<ASTNode,ASTNode> >::iterator itend = bm.NodeLetVarVec.end();
-
-      os << "(LET ";      
-      //print the let var first
-      it->first.PL_Print1(os,indentation,false);
-      os << " = ";
-      //print the expr
-      it->second.PL_Print1(os,indentation,false);
-
-      //update the second map for proper printing of LET
-      bm.NodeLetVarMap1[it->second] = it->first;
-
-      for(it++;it!=itend;it++) {
-        os << "," << endl;
-	//print the let var first
-	it->first.PL_Print1(os,indentation,false);
-	os << " = ";
-	//print the expr
-	it->second.PL_Print1(os,indentation,false);
-
-        //update the second map for proper printing of LET
-        bm.NodeLetVarMap1[it->second] = it->first;
-      }
-    
-      os << " IN " << endl;      
-      PL_Print1(os,indentation, true);
-      os << ") ";
-    }
-    else
-      PL_Print1(os,indentation, false);
-    //os << " )";
-    os << " ";
-    return os;
-  } //end of PL_Print()
-
-  //traverse "*this", and construct "let variables" for terms that
-  //occur more than once in "*this".
-  void ASTNode::LetizeNode(void) const {
-    Kind kind = this->GetKind();
-
-    if(kind == SYMBOL  || 
-       kind == BVCONST ||
-       kind == FALSE   ||
-       kind == TRUE)
-      return;
-
-    //FIXME: this is ugly.
-    BeevMgr& bm = GetBeevMgr();     
-    const ASTVec &c = this->GetChildren();
-    for(ASTVec::const_iterator it=c.begin(),itend=c.end();it!=itend;it++){
-      ASTNode ccc = *it;
-      if(bm.PLPrintNodeSet.find(ccc) == bm.PLPrintNodeSet.end()){
-	//If branch: if *it is not in NodeSet then,
-	//
-	//1. add it to NodeSet
-	//
-	//2. Letize its childNodes
-
-	//FIXME: Fetching BeevMgr is annoying.  Can we put this in
-	//some kind of a printer class
-	bm.PLPrintNodeSet.insert(ccc);
-	//debugging
-	//cerr << ccc;
-	ccc.LetizeNode();
-      } 
-      else{
-	Kind k = ccc.GetKind();
-	if(k == SYMBOL  || 
-	   k == BVCONST ||
-	   k == FALSE   ||
-	   k == TRUE)
-	  continue;
-	
-	//0. Else branch: Node has been seen before
-	//
-	//1. Check if the node has a corresponding letvar in the
-	//1. NodeLetVarMap.
-	//
-	//2. if no, then create a new var and add it to the
-	//2. NodeLetVarMap
-	if(bm.NodeLetVarMap.find(ccc) == bm.NodeLetVarMap.end()) {
-	  //Create a new symbol. Get some name. if it conflicts with a
-	  //declared name, too bad. 
-	  int sz = bm.NodeLetVarMap.size();
-	  ostringstream oss;
-	  oss << "let_k_" << sz;
-
-	  ASTNode CurrentSymbol = bm.CreateSymbol(oss.str().c_str());
-	  CurrentSymbol.SetValueWidth(this->GetValueWidth());
-	  CurrentSymbol.SetIndexWidth(this->GetIndexWidth());	  
-	  /* If for some reason the variable being created here is
-	   * already declared by the user then the printed output will
-	   * not be a legal input to the system. too bad. I refuse to
-	   * check for this.  [Vijay is the author of this comment.]
-	   */
-	  
-	  bm.NodeLetVarMap[ccc] = CurrentSymbol;
-	  std::pair<ASTNode,ASTNode> node_letvar_pair(CurrentSymbol,ccc);
-	  bm.NodeLetVarVec.push_back(node_letvar_pair);
-	}
-      }    
-    }
-  } //end of LetizeNode()
-
-  void ASTNode::PL_Print1(ostream& os,
-			  int indentation, 
-			  bool letize) const {
-    //os << spaces(indentation);
-    //os << endl << spaces(indentation);
-    if (!IsDefined()) {
-      os << "<undefined>";
-      return;
-    }
-    
-    //if this node is present in the letvar Map, then print the letvar
-    BeevMgr &bm = GetBeevMgr();
-
-    //this is to print letvars for shared subterms inside the printing
-    //of "(LET v0 = term1, v1=term1@term2,...
-    if((bm.NodeLetVarMap1.find(*this) != bm.NodeLetVarMap1.end()) && !letize) {
-      (bm.NodeLetVarMap1[*this]).PL_Print1(os,indentation,letize);
-      return;
-    }
-
-    //this is to print letvars for shared subterms inside the actual
-    //term to be printed
-    if((bm.NodeLetVarMap.find(*this) != bm.NodeLetVarMap.end()) && letize) {
-      (bm.NodeLetVarMap[*this]).PL_Print1(os,indentation,letize);
-      return;
-    }
-    
-    //otherwise print it normally
-    Kind kind = GetKind();
-    const ASTVec &c = GetChildren();     
-    switch(kind) {
-    case BVGETBIT:
-      c[0].PL_Print1(os,indentation,letize);
-      os << "{";
-      c[1].PL_Print1(os,indentation,letize);
-      os << "}";
-      break;
-    case BITVECTOR:
-      os << "BITVECTOR(";
-      unsigned char * str;
-      str = CONSTANTBV::BitVector_to_Hex(c[0].GetBVConst());
-      os << str << ")";
-      CONSTANTBV::BitVector_Dispose(str);
-      break;
-    case BOOLEAN:
-      os << "BOOLEAN";
-      break;
-    case FALSE:
-    case TRUE:
-      os << kind;
-      break;
-    case BVCONST:
-    case SYMBOL:
-      _int_node_ptr->nodeprint(os); 
-      break;
-    case READ:
-      c[0].PL_Print1(os, indentation,letize);
-      os << "[";
-      c[1].PL_Print1(os,indentation,letize);
-      os << "]";
-      break;
-    case WRITE:
-      os << "(";
-      c[0].PL_Print1(os,indentation,letize);
-      os << " WITH [";
-      c[1].PL_Print1(os,indentation,letize);
-      os << "] := ";
-      c[2].PL_Print1(os,indentation,letize);
-      os << ")";
-      os << endl;
-      break;
-    case BVUMINUS:
-      os << kind << "( ";
-      c[0].PL_Print1(os,indentation,letize);
-      os << ")";
-      break;
-    case NOT:
-      os << "NOT(";
-      c[0].PL_Print1(os,indentation,letize);
-      os << ") " << endl;
-      break;
-    case BVNEG:
-      os << " ~(";
-      c[0].PL_Print1(os,indentation,letize);
-      os << ")";
-      break;
-    case BVCONCAT:
-      os << "(";
-      c[0].PL_Print1(os,indentation,letize);
-      os << " @ ";
-      c[1].PL_Print1(os,indentation,letize);
-      os << ")" << endl;
-      break;
-    case BVOR:
-      os << "(";
-      c[0].PL_Print1(os,indentation,letize);
-      os << " | ";
-      c[1].PL_Print1(os,indentation,letize);
-      os << ")";
-      break;
-    case BVAND:
-      os << "(";
-      c[0].PL_Print1(os,indentation,letize);
-      os << " & ";
-      c[1].PL_Print1(os,indentation,letize);
-      os << ")";
-      break;
-    case BVEXTRACT:
-      c[0].PL_Print1(os,indentation,letize);
-      os << "[";
-      os << GetUnsignedConst(c[1]);
-      os << ":";
-      os << GetUnsignedConst(c[2]);
-      os << "]";
-      break;
-    case BVLEFTSHIFT:
-      os << "(";
-      c[0].PL_Print1(os,indentation,letize);
-      os << " << ";
-      os << GetUnsignedConst(c[1]);
-      os << ")";
-      break;
-    case BVRIGHTSHIFT:
-      os << "(";
-      c[0].PL_Print1(os,indentation,letize);
-      os << " >> ";
-      os << GetUnsignedConst(c[1]);
-      os << ")";
-      break;
-    case BVMULT:
-    case BVSUB:
-    case BVPLUS:
-    case SBVDIV:      
-    case SBVMOD:
-    case BVDIV:      
-    case BVMOD:
-      os << kind << "(";
-      os << this->GetValueWidth();
-      for(ASTVec::const_iterator it=c.begin(),itend=c.end();it!=itend;it++) {
-	os << ", " << endl;
-	it->PL_Print1(os,indentation,letize);	
-      }
-      os << ")" << endl;
-      break;    
-    case ITE:
-      os << "IF(";
-      c[0].PL_Print1(os,indentation,letize);
-      os << ")" << endl;
-      os << "THEN ";
-      c[1].PL_Print1(os,indentation,letize);
-      os << endl << "ELSE ";
-      c[2].PL_Print1(os,indentation,letize);
-      os << endl << "ENDIF";
-      break;
-    case BVLT:
-    case BVLE:
-    case BVGT:
-    case BVGE:
-    case BVXOR:
-    case BVNAND:
-    case BVNOR:
-    case BVXNOR:
-      os << kind << "(";
-      c[0].PL_Print1(os,indentation,letize);
-      os << ",";
-      c[1].PL_Print1(os,indentation,letize);
-      os << ")" << endl;
-      break;
-    case BVSLT:
-      os << "SBVLT" << "(";
-      c[0].PL_Print1(os,indentation,letize);
-      os << ",";
-      c[1].PL_Print1(os,indentation,letize);
-      os << ")" << endl;
-      break;
-    case BVSLE:
-      os << "SBVLE" << "(";
-      c[0].PL_Print1(os,indentation,letize);
-      os << ",";
-      c[1].PL_Print1(os,indentation,letize);
-      os << ")" << endl;
-      break;
-    case BVSGT:
-      os << "SBVGT" << "(";
-      c[0].PL_Print1(os,indentation,letize);
-      os << ",";
-      c[1].PL_Print1(os,indentation,letize);
-      os << ")" << endl;
-      break;
-    case BVSGE:
-      os << "SBVGE" << "(";
-      c[0].PL_Print1(os,indentation,letize);
-      os << ",";
-      c[1].PL_Print1(os,indentation,letize);
-      os << ")" << endl;
-      break;
-    case EQ:
-      c[0].PL_Print1(os,indentation,letize);
-      os << " = ";
-      c[1].PL_Print1(os,indentation,letize);      
-      os << endl;
-      break;
-    case NEQ:
-      c[0].PL_Print1(os,indentation,letize);
-      os << " /= ";
-      c[1].PL_Print1(os,indentation,letize);      
-      os << endl;
-      break;
-    case AND:
-    case OR:
-    case NAND:
-    case NOR:
-    case XOR: {
-      os << "(";
-      c[0].PL_Print1(os,indentation,letize);
-      ASTVec::const_iterator it=c.begin();
-      ASTVec::const_iterator itend=c.end();
-
-      it++;
-      for(;it!=itend;it++) {
-	os << " " << kind << " ";
-	it->PL_Print1(os,indentation,letize);
-	os << endl;
-      }
-      os << ")";
-      break;
-    }
-    case IFF:
-      os << "(";
-      os << "(";
-      c[0].PL_Print1(os,indentation,letize);
-      os << ")";
-      os << " <=> ";
-      os << "(";
-      c[1].PL_Print1(os,indentation,letize);      
-      os << ")";
-      os << ")";
-      os << endl;
-      break;
-    case IMPLIES:
-      os << "(";
-      os << "(";
-      c[0].PL_Print1(os,indentation,letize);
-      os << ")";
-      os << " => ";
-      os << "(";
-      c[1].PL_Print1(os,indentation,letize);
-      os << ")";
-      os << ")";
-      os << endl;
-      break;
-    case BVSX:
-      os << kind << "(";
-      c[0].PL_Print1(os,indentation,letize);
-      os << ",";
-      os << this->GetValueWidth();
-      os << ")" << endl;
-      break;
-    default:
-      //remember to use LispPrinter here. Otherwise this function will
-      //go into an infinite loop. Recall that "<<" is overloaded to
-      //the lisp printer. FatalError uses lispprinter
-      FatalError("PL_Print1: printing not implemented for this kind: ",*this);
-      break;
-    }
-  } //end of PL_Print1()
-
-  ////////////////////////////////////////////////////////////////
-  //  BeevMgr members
-  ////////////////////////////////////////////////////////////////
-  ASTNode BeevMgr::CreateNode(Kind kind, const ASTVec & back_children) {
-    // create a new node.  Children will be modified.
-    ASTInterior *n_ptr = new ASTInterior(kind, *this);
-
-    // insert all of children at end of new_children.
-    ASTNode n(CreateInteriorNode(kind, n_ptr, back_children));
-    return n;
-  }
-  
-  ASTNode BeevMgr::CreateNode(Kind kind,
-			      const ASTNode& child0,
-			      const ASTVec & back_children) {
-
-    ASTInterior *n_ptr = new ASTInterior(kind, *this);
-    ASTVec &front_children = n_ptr->_children;
-    front_children.push_back(child0);
-    ASTNode n(CreateInteriorNode(kind, n_ptr,  back_children));
-    return n;
-  }
-  
-  ASTNode BeevMgr::CreateNode(Kind kind,
-			      const ASTNode& child0,
-			      const ASTNode& child1,
-			      const ASTVec & back_children) {
-
-    ASTInterior *n_ptr = new ASTInterior(kind, *this);
-    ASTVec &front_children = n_ptr->_children;
-    front_children.push_back(child0);
-    front_children.push_back(child1);
-    ASTNode n(CreateInteriorNode(kind, n_ptr, back_children));
-    return n;
-  }
-  
-  
-  ASTNode BeevMgr::CreateNode(Kind kind,
-			      const ASTNode& child0,
-			      const ASTNode& child1,
-			      const ASTNode& child2,
-			      const ASTVec & back_children) {
-    ASTInterior *n_ptr = new ASTInterior(kind, *this);
-    ASTVec &front_children = n_ptr->_children;
-    front_children.push_back(child0);
-    front_children.push_back(child1);
-    front_children.push_back(child2);
-    ASTNode n(CreateInteriorNode(kind, n_ptr, back_children));
-    return n;
-  }
-  
-  
-  ASTInterior *BeevMgr::CreateInteriorNode(Kind kind,
-					   // children array of this node will be modified.
-					   ASTInterior *n_ptr,
-					   const ASTVec & back_children) {
-
-    // insert back_children at end of front_children
-    ASTVec &front_children = n_ptr->_children;
-
-    front_children.insert(front_children.end(), back_children.begin(), back_children.end());
-
-    // check for undefined nodes.
-    ASTVec::const_iterator it_end = front_children.end();
-    for (ASTVec::const_iterator it = front_children.begin(); it != it_end; it++) {
-      if (it->IsNull())
-	FatalError("CreateInteriorNode: Undefined childnode in CreateInteriorNode: ", ASTUndefined);      
-    }
-
-    return LookupOrCreateInterior(n_ptr);
-  }
-    
-  /** Trivial but virtual destructor */
-  ASTSymbol::~ASTSymbol() {}
-  
-  ostream &operator<<(ostream &os, const ASTNodeMap &nmap)
-  {
-    ASTNodeMap::const_iterator iend = nmap.end();
-    for (ASTNodeMap::const_iterator i = nmap.begin(); i!=iend; i++) {
-      os << "Key: " << i->first << endl;
-      os << "Value: " << i->second << endl;
-    }
-    return os;
-  }
-  
-  ////////////////////////////////////////////////////////////////
-  // BeevMgr member functions to create ASTSymbol and ASTBVConst
-  ////////////////////////////////////////////////////////////////
-  ASTNode BeevMgr::CreateSymbol(const char * const name) 
-  { 
-    ASTSymbol temp_sym(name, *this);
-    ASTNode n(LookupOrCreateSymbol(temp_sym));
-    return n;
-  }
-
-#ifndef NATIVE_C_ARITH
-  //Create a ASTBVConst node
-  ASTNode BeevMgr::CreateBVConst(unsigned int width, 
-				 unsigned long long int bvconst){ 
-    if(width == 0 || width > (sizeof(unsigned long long int)<<3))
-      FatalError("CreateBVConst: trying to create a bvconst of width: ", ASTUndefined, width);
-
-    CBV bv = CONSTANTBV::BitVector_Create(width, true);
-
-    // Copy bvconst in using at most MaxChunkSize chunks, starting with the
-    // least significant bits.
-    const uint32_t MaxChunkSize = 32;
-    for (unsigned offset = 0; offset != width;) {
-      uint32_t numbits = std::min(MaxChunkSize, width - offset);
-      uint32_t mask = ~0 >> (32 - numbits);
-      CONSTANTBV::BitVector_Chunk_Store(bv, numbits, offset, 
-                                        (bvconst >> offset) & mask);
-      offset += numbits;
-    }
-
-    return CreateBVConst(bv, width);
-  }
-
-  //Create a ASTBVConst node from std::string
-  ASTNode BeevMgr::CreateBVConst(const char* const strval, int base) {
-    size_t width = strlen((const char *)strval);    
-    if(!(2 == base || 10 == base || 16 == base)){
-      FatalError("CreateBVConst: unsupported base: ",ASTUndefined,base);
-    }
-    //FIXME Tim: Earlier versions of the code assume that the length of
-    //binary strings is 32 bits.
-    if(10 == base) width = 32;
-    if(16 == base) width = width * 4;
-
-    //checking if the input is in the correct format
-    CBV bv = CONSTANTBV::BitVector_Create(width,true);
-    CONSTANTBV::ErrCode e;
-    if(2 == base){
-      e = CONSTANTBV::BitVector_from_Bin(bv, (unsigned char*)strval);
-    }else if(10 == base){
-      e = CONSTANTBV::BitVector_from_Dec(bv, (unsigned char*)strval);
-    }else if(16 == base){
-      e = CONSTANTBV::BitVector_from_Hex(bv, (unsigned char*)strval);
-    }else{
-      e = CONSTANTBV::ErrCode_Pars;
-    }
-
-    if(0 != e) {
-      cerr << "CreateBVConst: " << BitVector_Error(e);
-      FatalError("",ASTUndefined);
-    }
-
-    //FIXME 
-    return CreateBVConst(bv, width);
-  }
-  
-
-  //FIXME Code currently assumes that it will destroy the bitvector passed to it
-  ASTNode BeevMgr::CreateBVConst(CBV bv, unsigned width){
-     ASTBVConst temp_bvconst(bv, width, *this);
-     ASTNode n(LookupOrCreateBVConst(temp_bvconst));
-     
-     CONSTANTBV::BitVector_Destroy(bv);
-     
-     return n;
-  }
-
-  ASTNode BeevMgr::CreateZeroConst(unsigned width) {
-    CBV z = CONSTANTBV::BitVector_Create(width, true);
-    return CreateBVConst(z, width);
-  }
-  
-  ASTNode BeevMgr::CreateOneConst(unsigned width) {
-    CBV o = CONSTANTBV::BitVector_Create(width, true);
-    CONSTANTBV::BitVector_increment(o);
-    
-    return CreateBVConst(o,width);
-  }
-
-  ASTNode BeevMgr::CreateTwoConst(unsigned width) {
-    CBV two = CONSTANTBV::BitVector_Create(width, true);
-    CONSTANTBV::BitVector_increment(two);
-    CONSTANTBV::BitVector_increment(two);
-
-    return CreateBVConst(two,width);
-  }
-
-  ASTNode BeevMgr::CreateMaxConst(unsigned width) {
-    CBV max = CONSTANTBV::BitVector_Create(width, false);
-    CONSTANTBV::BitVector_Fill(max);
-
-    return CreateBVConst(max,width);
-  }
-
-  //To ensure unique BVConst nodes, lookup the node in unique-table
-  //before creating a new one.
-  ASTBVConst *BeevMgr::LookupOrCreateBVConst(ASTBVConst &s) {
-    ASTBVConst *s_ptr = &s;  // it's a temporary key.
-    
-    // Do an explicit lookup to see if we need to create a copy of the string.    
-    ASTBVConstSet::const_iterator it;
-    if ((it = _bvconst_unique_table.find(s_ptr)) == _bvconst_unique_table.end()) {
-      // Make a new ASTBVConst with duplicated string (can't assign
-      // _name because it's const).  Can cast the iterator to
-      // non-const -- carefully.
-
-      ASTBVConst * s_copy = new ASTBVConst(s);      
-      s_copy->SetNodeNum(NewNodeNum());
-      
-      pair<ASTBVConstSet::const_iterator, bool> p = _bvconst_unique_table.insert(s_copy);
-      return *p.first;
-    }
-    else{
-      // return symbol found in table.
-      return *it;
-    }
-  }
-
-  // Inline because we need to wait until unique_table is defined
-  void ASTBVConst::CleanUp() {
-    //  cout << "Deleting node " << this->GetNodeNum() << endl;
-    _bm._bvconst_unique_table.erase(this);
-    delete this;
-  }
-
-  // Get the value of bvconst from a bvconst.  It's an error if kind != BVCONST
-  CBV ASTNode::GetBVConst() const {
-    if(GetKind() != BVCONST)
-      FatalError("GetBVConst: non bitvector-constant: ",*this);
-    return ((ASTBVConst *) _int_node_ptr)->GetBVConst();      
-  }
-#else
-  //Create a ASTBVConst node
-  ASTNode BeevMgr::CreateBVConst(const unsigned int width, 
-				 const unsigned long long int bvconst) { 
-    if(width > 64 || width <= 0)
-      FatalError("Fatal Error: CreateBVConst: trying to create a bvconst of width:", ASTUndefined, width);
-    
-    //64 bit mask
-    unsigned long long int mask = 0xffffffffffffffffLL;
-    mask = mask >> (64 - width);
-
-    unsigned long long int bv = bvconst;
-    bv = bv & mask;
-
-    ASTBVConst temp_bvconst(bv, *this);
-    temp_bvconst._value_width = width;    
-    ASTNode n(LookupOrCreateBVConst(temp_bvconst));
-    n.SetValueWidth(width);
-    n.SetIndexWidth(0);
-    return n;
-  }
-  //Create a ASTBVConst node from std::string
-  ASTNode BeevMgr::CreateBVConst(const char* strval, int base) {    
-    if(!(base == 2 || base == 16 || base == 10))
-      FatalError("CreateBVConst: This base is not supported: ", ASTUndefined, base);
-
-    if(10 != base) {
-      unsigned int width = (base == 2) ? strlen(strval) : strlen(strval)*4;
-      unsigned long long int val =  strtoull(strval, NULL, base);
-      ASTNode bvcon = CreateBVConst(width, val);
-      return bvcon;
-    }
-    else {
-      //this is an ugly hack to accomodate SMTLIB format
-      //restrictions. SMTLIB format represents bitvector constants in
-      //base 10 (what a terrible idea, but i have no choice but to
-      //support it), and make an implicit assumption that the length
-      //is 32 (another terrible idea).
-      unsigned width = 32;
-      unsigned long long int val = strtoull(strval, NULL, base);
-      ASTNode bvcon = CreateBVConst(width, val);
-      return bvcon;
-    }
-  }
-  
-  //To ensure unique BVConst nodes, lookup the node in unique-table
-  //before creating a new one.
-  ASTBVConst *BeevMgr::LookupOrCreateBVConst(ASTBVConst &s) {
-    ASTBVConst *s_ptr = &s;	// it's a temporary key.
-
-    // Do an explicit lookup to see if we need to create a copy of the
-    // string.
-    ASTBVConstSet::const_iterator it;
-    if ((it = _bvconst_unique_table.find(s_ptr)) == _bvconst_unique_table.end()) {
-      // Make a new ASTBVConst. Can cast the iterator to non-const --
-      // carefully.
-      unsigned int width = s_ptr->_value_width;
-      ASTBVConst * s_ptr1 = new ASTBVConst(s_ptr->GetBVConst(), *this);
-      s_ptr1->SetNodeNum(NewNodeNum());
-      s_ptr1->_value_width = width;
-      pair<ASTBVConstSet::const_iterator, bool> p = _bvconst_unique_table.insert(s_ptr1);
-      return *p.first;
-    }
-    else
-      // return BVConst found in table.
-      return *it;
-  }
-
-  // Inline because we need to wait until unique_table is defined
-  void ASTBVConst::CleanUp() {
-    //  cout << "Deleting node " << this->GetNodeNum() << endl;
-    _bm._bvconst_unique_table.erase(this);
-    delete this;
-  }
-
-  // Get the value of bvconst from a bvconst.  It's an error if kind
-  // != BVCONST
-  unsigned long long int ASTNode::GetBVConst() const {
-    if(GetKind() != BVCONST)
-      FatalError("GetBVConst: non bitvector-constant: ", *this);
-    return ((ASTBVConstTmp *) _int_node_ptr)->GetBVConst();
-  }
-
-  ASTNode BeevMgr::CreateZeroConst(unsigned width) {
-    return CreateBVConst(width,0);
-  }
-  
-  ASTNode BeevMgr::CreateOneConst(unsigned width) {
-    return CreateBVConst(width,1);
-  }
-
-  ASTNode BeevMgr::CreateTwoConst(unsigned width) {
-    return CreateBVConst(width,2);
-  }
-
-  ASTNode BeevMgr::CreateMaxConst(unsigned width) {
-    std::string s;
-    s.insert(s.end(),width,'1');
-    return CreateBVConst(s.c_str(),2);
-  }
-
-#endif  
-
-  // FIXME: _name is now a constant field, and this assigns to it
-  // because it tries not to copy the string unless it needs to.  How
-  // do I avoid copying children in ASTInterior?  Perhaps I don't!
-  
-  // Note: There seems to be a limitation of hash_set, in that insert
-  // returns a const iterator to the value.  That prevents us from
-  // modifying the name (in a hash-preserving way) after the symbol is
-  // inserted.  FIXME: Is there a way to do this with insert?  Need a
-  // function to make a new object in the middle of insert.  Read STL
-  // documentation.
-  
-  ASTSymbol *BeevMgr::LookupOrCreateSymbol(ASTSymbol& s) {
-    ASTSymbol *s_ptr = &s;  // it's a temporary key.
-    
-    // Do an explicit lookup to see if we need to create a copy of the string.    
-    ASTSymbolSet::const_iterator it;
-    if ((it = _symbol_unique_table.find(s_ptr)) == _symbol_unique_table.end()) {
-      // Make a new ASTSymbol with duplicated string (can't assign
-      // _name because it's const).  Can cast the iterator to
-      // non-const -- carefully.
-      //std::string strname(s_ptr->GetName());
-      ASTSymbol * s_ptr1 = new ASTSymbol(strdup(s_ptr->GetName()), *this);
-      s_ptr1->SetNodeNum(NewNodeNum());
-      s_ptr1->_value_width = s_ptr->_value_width;
-      pair<ASTSymbolSet::const_iterator, bool> p = _symbol_unique_table.insert(s_ptr1);
-      return *p.first;
-    }
-    else
-      // return symbol found in table.
-      return *it;    
-  }
-
-  bool BeevMgr::LookupSymbol(ASTSymbol& s) {
-    ASTSymbol* s_ptr = &s;  // it's a temporary key.
-
-    if(_symbol_unique_table.find(s_ptr) == _symbol_unique_table.end()) 
-      return false;
-    else
-      return true;
-  }
-
-  // Inline because we need to wait until unique_table is defined
-  void ASTSymbol::CleanUp() {
-    //  cout << "Deleting node " << this->GetNodeNum() << endl;
-    _bm._symbol_unique_table.erase(this);
-    //FIXME This is a HUGE free to invoke.
-    //TEST IT!
-    free((char*) this->_name);
-    delete this;
-  }
-  
-  ////////////////////////////////////////////////////////////////
-  //
-  //  IO manipulators for Lisp format printing of AST.
-  //
-  ////////////////////////////////////////////////////////////////
-  
-  // FIXME: Additional controls
-  //   * Print node numbers  (addresses/nums)
-  //   * Printlength limit
-  //   * Printdepth limit
-  
-  /** Print a vector of ASTNodes in lisp format */
-  ostream &LispPrintVec(ostream &os, const ASTVec &v, int indentation)
-  {
-    // Print the children
-    ASTVec::const_iterator iend = v.end();
-    for (ASTVec::const_iterator i = v.begin(); i != iend; i++) {
-      i->LispPrint_indent(os, indentation);
-    }
-    return os;
-  }
-
-  // FIXME: Made non-ref in the hope that it would work better.
-  void lp(ASTNode node)
-  {
-    cout << lisp(node) << endl;
-  }
-
-  void lpvec(const ASTVec &vec)
-  {
-    vec[0].GetBeevMgr().AlreadyPrintedSet.clear();
-    LispPrintVec(cout, vec, 0);
-    cout << endl;
-  }
-
-  // Copy constructor.  Maintain _ref_count
-  ASTNode::ASTNode(const ASTNode &n) : _int_node_ptr(n._int_node_ptr) {
-#ifndef SMTLIB    
-    if (n._int_node_ptr) {
-      n._int_node_ptr->IncRef();
-    }
-#endif
-  }
-  
-
-  /* FUNCTION: Typechecker for terms and formulas
-   * 
-   * TypeChecker: Assumes that the immediate Children of the input
-   * ASTNode have been typechecked. This function is suitable in
-   * scenarios like where you are building the ASTNode Tree, and you
-   * typecheck as you go along. It is not suitable as a general
-   * typechecker      
-   */
-  void BeevMgr::BVTypeCheck(const ASTNode& n) {
-    Kind k = n.GetKind();
-    //The children of bitvector terms are in turn bitvectors.
-    ASTVec v = n.GetChildren();
-    if(is_Term_kind(k)) {
-      switch(k) {
-      case BVCONST:
-	if(BITVECTOR_TYPE != n.GetType())
-	  FatalError("BVTypeCheck: The term t does not typecheck, where t = \n",n);
-	break;
-      case SYMBOL:
-	return;
-      case ITE:     
-	if(BOOLEAN_TYPE != n[0].GetType() && 
-	   BITVECTOR_TYPE != n[1].GetType() &&
-	   BITVECTOR_TYPE != n[2].GetType())
-	  FatalError("BVTypeCheck: The term t does not typecheck, where t = \n",n);
-	if(n[1].GetValueWidth() != n[2].GetValueWidth())
-	  FatalError("BVTypeCheck: length of THENbranch != length of ELSEbranch in the term t = \n",n);
-	if(n[1].GetIndexWidth() != n[2].GetIndexWidth())
-	  FatalError("BVTypeCheck: length of THENbranch != length of ELSEbranch in the term t = \n",n);
-	break;
-      case READ:
-	if(n[0].GetIndexWidth() != n[1].GetValueWidth()) {
-	  cerr << "Length of indexwidth of array: " << n[0] << " is : " << n[0].GetIndexWidth() << endl;
-	  cerr << "Length of the actual index is: " << n[1] << " is : " << n[1].GetValueWidth() << endl;
-	  FatalError("BVTypeCheck: length of indexwidth of array != length of actual index in the term t = \n",n);
-	}
-	break;      
-      case WRITE:
-	if(n[0].GetIndexWidth() != n[1].GetValueWidth())
-	  FatalError("BVTypeCheck: length of indexwidth of array != length of actual index in the term t = \n",n);
-	if(n[0].GetValueWidth() != n[2].GetValueWidth())
-	  FatalError("BVTypeCheck: valuewidth of array != length of actual value in the term t = \n",n);
-	break;      
-      case BVOR:
-      case BVAND:
-      case BVXOR:
-      case BVNOR:
-      case BVNAND:
-      case BVXNOR: 
-      case BVPLUS: 
-      case BVMULT:
-      case BVDIV:
-      case BVMOD:
-      case BVSUB: {
-	if(!(v.size() >= 2))
-	  FatalError("BVTypeCheck:bitwise Booleans and BV arith operators must have atleast two arguments\n",n);
-	unsigned int width = n.GetValueWidth();
-	for(ASTVec::iterator it=v.begin(),itend=v.end();it!=itend;it++){
-	  if(width != it->GetValueWidth()) {
-	    cerr << "BVTypeCheck:Operands of bitwise-Booleans and BV arith operators must be of equal length\n";
-	    cerr << n << endl;
-	    cerr << "width of term:" << width << endl;
-	    cerr << "width of offending operand:" << it->GetValueWidth() << endl;
-	    FatalError("BVTypeCheck:Offending operand:\n",*it);
-	  }
-	  if(BITVECTOR_TYPE != it->GetType())
-	    FatalError("BVTypeCheck: ChildNodes of bitvector-terms must be bitvectors\n",n);
-	}
-	break;
-      }
-      case BVSX:
-	//in BVSX(n[0],len), the length of the BVSX term must be
-	//greater than the length of n[0]
-	if(n[0].GetValueWidth() >= n.GetValueWidth()) {
-	  FatalError("BVTypeCheck: BVSX(t,bvsx_len) : length of 't' must be <= bvsx_len\n",n);
-	} 
-	break;
-      default:
-	for(ASTVec::iterator it=v.begin(),itend=v.end();it!=itend;it++)
-	  if(BITVECTOR_TYPE != it->GetType()) {
-	    cerr << "The type is: " << it->GetType() << endl;
-	    FatalError("BVTypeCheck:ChildNodes of bitvector-terms must be bitvectors\n",n);
-	  }
-	break;
-      }
-      
-      switch(k) {
-      case BVCONCAT:
-	if(n.Degree() != 2)
-	  FatalError("BVTypeCheck: should have exactly 2 args\n",n);
-	if(n.GetValueWidth() != n[0].GetValueWidth() + n[1].GetValueWidth())
-	  FatalError("BVTypeCheck:BVCONCAT: lengths do not add up\n",n);	
-	break;
-      case BVUMINUS:
-      case BVNEG:
-	if(n.Degree() != 1)
-	  FatalError("BVTypeCheck: should have exactly 1 args\n",n);
-	break;
-      case BVEXTRACT:
-	if(n.Degree() != 3)
-	  FatalError("BVTypeCheck: should have exactly 3 args\n",n);
-	if(!(BVCONST == n[1].GetKind() && BVCONST == n[2].GetKind()))
-	  FatalError("BVTypeCheck: indices should be BVCONST\n",n);
-	if(n.GetValueWidth() != GetUnsignedConst(n[1])- GetUnsignedConst(n[2])+1)
-	  FatalError("BVTypeCheck: length mismatch\n",n);
-	break;
-      case BVLEFTSHIFT:
-      case BVRIGHTSHIFT:
-	if(n.Degree() != 2)
-	  FatalError("BVTypeCheck: should have exactly 2 args\n",n);
-	break;
-	//case BVVARSHIFT:
-	//case BVSRSHIFT:
-	break;
-      default:
-	break;
-      }
-    }
-    else {
-      if(!(is_Form_kind(k) && BOOLEAN_TYPE == n.GetType()))
-	FatalError("BVTypeCheck: not a formula:",n);
-      switch(k){
-      case TRUE:
-      case FALSE:
-      case SYMBOL:
-	return;
-      case EQ:
-      case NEQ:	 
-	if(!(n[0].GetValueWidth() == n[1].GetValueWidth() &&
-	     n[0].GetIndexWidth() == n[1].GetIndexWidth())) {
-	  cerr << "valuewidth of lhs of EQ: " << n[0].GetValueWidth() << endl;
-	  cerr << "valuewidth of rhs of EQ: " << n[1].GetValueWidth() << endl;
-	  cerr << "indexwidth of lhs of EQ: " << n[0].GetIndexWidth() << endl;
-	  cerr << "indexwidth of rhs of EQ: " << n[1].GetIndexWidth() << endl;
-	  FatalError("BVTypeCheck: terms in atomic formulas must be of equal length",n);
-	}
-	break;
-      case BVLT:
-      case BVLE:
-      case BVGT:
-      case BVGE:
-      case BVSLT:
-      case BVSLE:
-      case BVSGT:
-      case BVSGE:	
-	if(BITVECTOR_TYPE != n[0].GetType() && BITVECTOR_TYPE != n[1].GetType())
-	  FatalError("BVTypeCheck: terms in atomic formulas must be bitvectors",n);
-	if(n[0].GetValueWidth() != n[1].GetValueWidth())
-	  FatalError("BVTypeCheck: terms in atomic formulas must be of equal length",n);
-	if(n[0].GetIndexWidth() != n[1].GetIndexWidth())
-	  FatalError("BVTypeCheck: terms in atomic formulas must be of equal length",n);
-	break;
-      case NOT:
-	if(1 != n.Degree())
-	  FatalError("BVTypeCheck: NOT formula can have exactly one childNode",n);
-	break;
-      case AND:
-      case OR:
-      case XOR:
-      case NAND:
-      case NOR:
-	if(2 > n.Degree())
-	  FatalError("BVTypeCheck: AND/OR/XOR/NAND/NOR: must have atleast 2 ChildNodes",n);
-	break;
-      case IFF:
-      case IMPLIES:	
-	if(2 != n.Degree())
-	  FatalError("BVTypeCheck:IFF/IMPLIES must have exactly 2 ChildNodes",n);
-	break;
-      case ITE:
-	if(3 != n.Degree())
-	  FatalError("BVTypeCheck:ITE must have exactly 3 ChildNodes",n);		
-	break;
-      default:
-	FatalError("BVTypeCheck: Unrecognized kind: ",ASTUndefined);
-	break;
-      }
-    }
-  } //End of TypeCheck function
-
-  //add an assertion to the current logical context
-  void BeevMgr::AddAssert(const ASTNode& assert) {
-    if(!(is_Form_kind(assert.GetKind()) && BOOLEAN_TYPE == assert.GetType())) {
-      FatalError("AddAssert:Trying to assert a non-formula:",assert);
-    }
-      
-    ASTVec * v;
-    //if the stack of ASTVec is not empty, then take the top ASTVec
-    //and add the input assert to it
-    if(!_asserts.empty()) {
-      v = _asserts.back();
-      //v->push_back(TransformFormula(assert));
-      v->push_back(assert);
-    }
-    else {
-      //else create a logical context, and add it to the top of the
-      //stack
-      v = new ASTVec();
-      //v->push_back(TransformFormula(assert));
-      v->push_back(assert);
-      _asserts.push_back(v);	
-    }
-  }
-  
-  void BeevMgr::Push(void) {
-    ASTVec * v;
-    v = new ASTVec();
-    _asserts.push_back(v);
-  }
-  
-  void BeevMgr::Pop(void) {
-    if(!_asserts.empty()) {
-       ASTVec * c = _asserts.back();
-             //by calling the clear function we ensure that the ref count is
-             //decremented for the ASTNodes stored in c
-             c->clear();
-             delete c;
-      _asserts.pop_back();
-    }
-  }
-
-  void BeevMgr::AddQuery(const ASTNode& q) {
-    //_current_query = TransformFormula(q);
-    //cerr << "\nThe current query is: " << q << endl;
-    _current_query = q;
-  }
-    
-  const ASTNode BeevMgr::PopQuery() {
-    ASTNode q = _current_query;
-    _current_query = ASTTrue;
-    return q;
-  }
-   
-  const ASTNode BeevMgr::GetQuery() {
-    return _current_query;
-  }
-  
-  const ASTVec BeevMgr::GetAsserts(void) {
-    vector<ASTVec *>::iterator it = _asserts.begin();
-    vector<ASTVec *>::iterator itend = _asserts.end();
-    
-    ASTVec v;
-    for(;it!=itend;it++) {
-      if(!(*it)->empty())
-	  v.insert(v.end(),(*it)->begin(),(*it)->end());
-    }
-    return v;
-  }
-
-  //Create a new variable of ValueWidth 'n'
-  ASTNode BeevMgr::NewArrayVar(unsigned int index, unsigned int value) {
-    std:: string c("v");
-    char d[32];
-    sprintf(d,"%d",_symbol_count++);
-    std::string ccc(d);
-    c += "_writearray_" + ccc;
-    
-    ASTNode CurrentSymbol = CreateSymbol(c.c_str());
-    CurrentSymbol.SetValueWidth(value);
-    CurrentSymbol.SetIndexWidth(index);
-    return CurrentSymbol;
-  } //end of NewArrayVar()
-
-
-  //Create a new variable of ValueWidth 'n'
-  ASTNode BeevMgr::NewVar(unsigned int value) {
-    std:: string c("v");
-    char d[32];
-    sprintf(d,"%d",_symbol_count++);
-    std::string ccc(d);
-    c += "_new_stp_var_" + ccc;
-    
-    ASTNode CurrentSymbol = CreateSymbol(c.c_str());
-    CurrentSymbol.SetValueWidth(value);
-    CurrentSymbol.SetIndexWidth(0);
-    _introduced_symbols.insert(CurrentSymbol);
-    return CurrentSymbol;
-  } //end of NewVar()
-
-  //prints statistics for the ASTNode
-  void BeevMgr::ASTNodeStats(const char * c, const ASTNode& a){
-    if(!stats)
-      return;
-
-    StatInfoSet.clear();
-    //print node size:
-    cout << endl << "Printing: " << c;
-    if(print_nodes) {
-      //a.PL_Print(cout,0);
-      //cout << endl;
-      cout << a << endl;
-    }
-    cout << "Node size is: ";
-    cout << NodeSize(a) << endl << endl;    
-  }
-
-  unsigned int BeevMgr::NodeSize(const ASTNode& a, bool clearStatInfo) {    
-    if(clearStatInfo)
-      StatInfoSet.clear();
-
-    ASTNodeSet::iterator it;
-    if((it = StatInfoSet.find(a)) != StatInfoSet.end())
-      //has already been counted
-      return 0;
-
-    //record that you have seen this node already
-    StatInfoSet.insert(a);
-    
-    //leaf node has a size of 1
-    if(a.Degree() == 0)
-      return 1;
-
-    unsigned newn = 1;
-    ASTVec c = a.GetChildren();
-    for(ASTVec::iterator it=c.begin(),itend=c.end();it!=itend;it++)
-      newn += NodeSize(*it);
-    return newn;
-  }
-
-  void BeevMgr::ClearAllTables(void) {
-    //clear all tables before calling toplevelsat
-    _ASTNode_to_SATVar.clear();
-    _SATVar_to_AST.clear();
-
-    for(ASTtoBitvectorMap::iterator it=_ASTNode_to_Bitvector.begin(),
-	  itend=_ASTNode_to_Bitvector.end();it!=itend;it++) {
-      delete it->second;
-    }
-    _ASTNode_to_Bitvector.clear();
-    
-    /* OLD Destructor
-     * for(ASTNodeToVecMap::iterator ivec = BBTermMemo.begin(),
-	  ivec_end=BBTermMemo.end();ivec!=ivec_end;ivec++) {
-      ivec->second.clear();
-    }*/
-
-    /*What should I do here? For ASTNodes?
-     * for(ASTNodeMap::iterator ivec = BBTermMemo.begin(),
-	  ivec_end=BBTermMemo.end();ivec!=ivec_end;ivec++) {
-      ivec->second.clear();
-    }*/
-    BBTermMemo.clear();
-    BBFormMemo.clear();
-    NodeLetVarMap.clear();
-    NodeLetVarMap1.clear();
-    PLPrintNodeSet.clear();
-    AlreadyPrintedSet.clear();
-    SimplifyMap.clear();
-    SimplifyNegMap.clear();
-    SolverMap.clear();
-    AlwaysTrueFormMap.clear();
-    _arrayread_ite.clear();
-    _arrayread_symbol.clear();
-    _introduced_symbols.clear();
-    TransformMap.clear();
-    _letid_expr_map.clear();
-    CounterExampleMap.clear();
-    ComputeFormulaMap.clear();
-    StatInfoSet.clear();
-
-    // for(std::vector<ASTVec *>::iterator it=_asserts.begin(),
-    // 	  itend=_asserts.end();it!=itend;it++) {
-    //       (*it)->clear();
-    //     }
-    _asserts.clear();
-    for(ASTNodeToVecMap::iterator iset = _arrayname_readindices.begin(), 
-	  iset_end = _arrayname_readindices.end();
-	iset!=iset_end;iset++) {
-      iset->second.clear();
-    }
-
-    _arrayname_readindices.clear();
-    _interior_unique_table.clear();
-    _symbol_unique_table.clear();
-    _bvconst_unique_table.clear();
-  }
-
-  void BeevMgr::ClearAllCaches(void) {
-    //clear all tables before calling toplevelsat
-    _ASTNode_to_SATVar.clear();
-    _SATVar_to_AST.clear();
-
-
-    for(ASTtoBitvectorMap::iterator it=_ASTNode_to_Bitvector.begin(),
-	  itend=_ASTNode_to_Bitvector.end();it!=itend;it++) {
-      delete it->second;
-    }
-    _ASTNode_to_Bitvector.clear();
-    
-    /*OLD destructor
-     * for(ASTNodeToVecMap::iterator ivec = BBTermMemo.begin(),
-	  ivec_end=BBTermMemo.end();ivec!=ivec_end;ivec++) {
-      ivec->second.clear();
-    }*/
-
-    /*What should I do here?
-     *for(ASTNodeMap::iterator ivec = BBTermMemo.begin(),
-	  ivec_end=BBTermMemo.end();ivec!=ivec_end;ivec++) {
-      ivec->second.clear();
-    }*/
-    BBTermMemo.clear();
-    BBFormMemo.clear();
-    NodeLetVarMap.clear();
-    NodeLetVarMap1.clear();
-    PLPrintNodeSet.clear();
-    AlreadyPrintedSet.clear();
-    SimplifyMap.clear();
-    SimplifyNegMap.clear();
-    SolverMap.clear();
-    AlwaysTrueFormMap.clear();
-    _arrayread_ite.clear();
-    _arrayread_symbol.clear();
-    _introduced_symbols.clear();
-    TransformMap.clear();
-    _letid_expr_map.clear();
-    CounterExampleMap.clear();
-    ComputeFormulaMap.clear();
-    StatInfoSet.clear();
-
-    for(ASTNodeToVecMap::iterator iset = _arrayname_readindices.begin(), 
-	  iset_end = _arrayname_readindices.end();
-	iset!=iset_end;iset++) {
-      iset->second.clear();
-    }
-
-    _arrayname_readindices.clear();
-    //_interior_unique_table.clear();
-    //_symbol_unique_table.clear();
-    //_bvconst_unique_table.clear();
-  }
-
-  void BeevMgr::CopySolverMap_To_CounterExample(void) {
-    if(!SolverMap.empty()) {
-      CounterExampleMap.insert(SolverMap.begin(),SolverMap.end());
-    }
-  }
-
-  void FatalError(const char * str, const ASTNode& a, int w) {
-    if(a.GetKind() != UNDEFINED) {
-      cerr << "Fatal Error: " << str << endl << a << endl;
-      cerr << w << endl;
-    }
-    else {
-      cerr << "Fatal Error: " << str << endl;
-      cerr << w << endl;
-    }
-    if (vc_error_hdlr)
-      vc_error_hdlr(str);
-    exit(-1);
-    //assert(0);
-  }
-
-  void FatalError(const char * str) {
-    cerr << "Fatal Error: " << str << endl;
-    if (vc_error_hdlr)
-      vc_error_hdlr(str);
-    exit(-1);
-    //assert(0);
-  }
-
-  //Variable Order Printer: A global function which converts a MINISAT
-  //var into a ASTNODE var. It then prints this var along with
-  //variable order dcisions taken by MINISAT.
-  void Convert_MINISATVar_To_ASTNode_Print(int minisat_var, 
-  					   int decision_level, int polarity) {
-    BEEV::ASTNode vv = globalBeevMgr_for_parser->_SATVar_to_AST[minisat_var];
-    cout << spaces(decision_level);
-    if(polarity) {
-      cout << "!";
-    }
-    vv.PL_Print(cout,0);
-    cout << endl;
-  }
-
-  void SortByExprNum(ASTVec& v) {
-    sort(v.begin(), v.end(), exprless);
-  }
-
-  bool isAtomic(Kind kind) {
-    if(TRUE == kind ||
-       FALSE == kind ||
-       EQ == kind ||
-       NEQ == kind ||
-       BVLT == kind ||
-       BVLE == kind ||
-       BVGT == kind ||
-       BVGE == kind ||
-       BVSLT == kind ||
-       BVSLE == kind ||
-       BVSGT == kind ||
-       BVSGE == kind ||
-       SYMBOL == kind ||
-       BVGETBIT == kind)
-      return true;
-    return false;
-  }
-
-  BeevMgr::~BeevMgr() {
-    ClearAllTables();
-  }
-} // end namespace
-
diff --git a/stp/AST/AST.h b/stp/AST/AST.h
deleted file mode 100644
index 3052107f..00000000
--- a/stp/AST/AST.h
+++ /dev/null
@@ -1,1806 +0,0 @@
-// -*- c++ -*-
-/********************************************************************
- * AUTHORS: Vijay Ganesh, David L. Dill
- *
- * BEGIN DATE: November, 2005
- *
- * LICENSE: Please view LICENSE file in the home dir of this Program
- ********************************************************************/
-
-#ifndef AST_H
-#define AST_H
-#include <vector>
-#ifdef EXT_HASH_MAP
-#include <ext/hash_set>
-#include <ext/hash_map>
-#else
-#include <hash_set>
-#include <hash_map>
-#endif
-#include <iostream>
-#include <sstream>
-#include <string>
-#include <map>
-#include <set>
-#include "ASTUtil.h"
-#include "ASTKind.h"
-#include "../sat/Solver.h"
-#include "../sat/SolverTypes.h"
-#include <cstdlib>
-#include <stdint.h>
-#ifndef NATIVE_C_ARITH
-#include "../constantbv/constantbv.h"
-#endif
-/*****************************************************************************
- * LIST OF CLASSES DECLARED IN THIS FILE:
- *
- * class BeevMgr;  
- * class ASTNode; 
- * class ASTInternal;  
- * class ASTInterior;  
- * class ASTSymbol;
- * class ASTBVConst;
- *****************************************************************************/
-namespace BEEV {
-  using namespace std; 
-  using namespace MINISAT;
-#ifdef EXT_HASH_MAP
-  using namespace __gnu_cxx;
-#endif
-
-  //return types for the GetType() function in ASTNode class
-  enum types {
-    BOOLEAN_TYPE = 0,
-    BITVECTOR_TYPE,
-    ARRAY_TYPE,
-    UNKNOWN_TYPE
-  };
-  
-  class BeevMgr;  
-  class ASTNode; 
-  class ASTInternal;  
-  class ASTInterior;  
-  class ASTSymbol;
-  class ASTBVConst;
-  class BVSolver;
-
-  //Vector of ASTNodes, used for child nodes among other things.  
-  typedef vector<ASTNode> ASTVec;
-  extern ASTVec _empty_ASTVec;
-  extern BeevMgr * globalBeevMgr_for_parser;
-
-  typedef unsigned int * CBV;
-
-  /***************************************************************************/
-  /*  Class ASTNode: Smart pointer to actual ASTNode internal datastructure. */
-  /***************************************************************************/
-  class ASTNode {
-    friend class BeevMgr;
-    friend class vector<ASTNode>;
-    //Print the arguments in lisp format.
-    friend ostream &LispPrintVec(ostream &os, 
-				 const ASTVec &v, int indentation = 0); 
-
-  private:
-    // FIXME: make this into a reference?
-    ASTInternal * _int_node_ptr;	// The real data.
-
-    // Usual constructor.  
-    ASTNode(ASTInternal *in);
-
-    //Check if it points to a null node
-    bool IsNull () const { return _int_node_ptr == NULL; }
-
-    //Equal iff ASTIntNode pointers are the same.
-    friend bool operator==(const ASTNode node1, const ASTNode node2){
-      return ((size_t) node1._int_node_ptr) == ((size_t) node2._int_node_ptr);
-    }
-    
-    /* FIXME:  Nondeterministic code *** */
-    /** questionable pointer comparison function */
-    friend bool operator<(const ASTNode node1, const ASTNode node2){
-      return ((size_t) node1._int_node_ptr) < ((size_t) node2._int_node_ptr);
-    }
-
-  public:
-    // This is for sorting by expression number (used in Boolean
-    //optimization)
-    friend bool exprless(const ASTNode n1, const ASTNode n2) {
-      Kind k1 = n1.GetKind();
-      Kind k2 = n2.GetKind();
-      
-      if(BVCONST == k1 && BVCONST != k2){
-	return true;
-      }
-      if(BVCONST != k1 && BVCONST == k2){
-	return false;
-      }
-      
-      if(SYMBOL == k1 && SYMBOL != k2) {
-      	return true;
-      }
-      
-      if(SYMBOL != k1 && SYMBOL == k2) {
-      	return false;
-      }
-
-      return (n1.GetNodeNum() < n2.GetNodeNum());
-    }//end of exprless 
-    
-    // Internal lisp-form printer that does not clear _node_print_table
-    ostream &LispPrint1(ostream &os, int indentation) const;
-
-    ostream &LispPrint_indent(ostream &os, int indentation) const;
-
-    // For lisp DAG printing.  Has it been printed already, so we can
-    // just print the node number?
-    bool IsAlreadyPrinted() const;
-    void MarkAlreadyPrinted() const;
-
-  public:
-    // Default constructor.  This gets used when declaring an ASTVec
-    // of a given size, in the hash table, etc.  For faster
-    // refcounting, create a symbol node for NULL.  Give it a big
-    // initial refcount.  Never free it.  also check, for ref-count
-    // overflow?
-    ASTNode() : _int_node_ptr(NULL) { };
-
-    // Copy constructor
-    ASTNode(const ASTNode &n);
-
-    // Destructor
-    ~ASTNode();
-
-    // Assignment (for ref counting)
-    ASTNode& operator=(const ASTNode& n);
-
-    BeevMgr &GetBeevMgr() const;
-
-    // Access node number
-    int GetNodeNum() const;
-
-    // Access kind.  Inlined later because of declaration ordering problems.
-    Kind GetKind() const;
-
-    // access Children
-    const ASTVec &GetChildren() const;
-    
-    // Return the number of child nodes
-    size_t Degree() const{ 
-      return GetChildren().size(); 
-    };    
-
-    // Get indexth childNode.
-    const ASTNode operator[](size_t index) const { 
-      return GetChildren()[index]; 
-    };    
-
-    // Get begin() iterator for child nodes
-    ASTVec::const_iterator begin() const{ 
-      return GetChildren().begin(); 
-    };  
-
-    // Get end() iterator for child nodes
-    ASTVec::const_iterator end() const{ 
-      return GetChildren().end(); 
-    };
-
-    //Get back() element for child nodes
-    const ASTNode back() const{
-      return GetChildren().back();
-    };  
-
-    // Get the name from a symbol (char *).  It's an error if kind != SYMBOL
-    const char *GetName() const;
-
-    //Get the BVCONST value
-#ifndef NATIVE_C_ARITH
-    CBV GetBVConst() const;
-#else
-    unsigned long long int GetBVConst() const;
-#endif
-
-    /*ASTNode is of type BV <==> ((indexwidth=0)&&(valuewidth>0))
-     *
-     *ASTNode is of type ARRAY <==> ((indexwidth>0)&&(valuewidth>0))
-     *
-     *ASTNode is of type BOOLEAN <==> ((indexwidth=0)&&(valuewidth=0))
-     *
-     *both indexwidth and valuewidth should never be less than 0
-     */
-    unsigned int GetIndexWidth () const;
-
-    // FIXME: This function is dangerous.  Try to eliminate it's use.
-    void SetIndexWidth (unsigned int iw) const;
-
-    unsigned int GetValueWidth () const;
-
-    // FIXME: This function is dangerous.  Try to eliminate it's use.
-    void SetValueWidth (unsigned int vw) const;
-
-    //return the type of the ASTNode
-    //0 iff BOOLEAN
-    //1 iff BITVECTOR
-    //2 iff ARRAY
-
-    /*ASTNode is of type BV <==> ((indexwidth=0)&&(valuewidth>0))
-     *
-     *ASTNode is of type ARRAY <==> ((indexwidth>0)&&(valuewidth>0))
-     *
-     *ASTNode is of type BOOLEAN <==> ((indexwidth=0)&&(valuewidth=0))
-     *
-     *both indexwidth and valuewidth should never be less than 0
-     */    
-    types GetType(void) const;
-
-    // Hash is pointer value of _int_node_ptr.
-    size_t Hash() const{ 
-      return (size_t) _int_node_ptr; 
-      //return GetNodeNum(); 
-    }
-
-    // lisp-form printer 
-    ostream& LispPrint(ostream &os, int indentation = 0) const;
-
-    //Presentation Language Printer
-    ostream& PL_Print(ostream &os, int indentation = 0) const;
-
-    void PL_Print1(ostream &os, int indentation = 0, bool b = false) const;
-
-    //Construct let variables for shared subterms
-    void LetizeNode(void) const;
-
-    // Attempt to define something that will work in the gdb
-    friend void lp(ASTNode &node);
-    friend void lpvec(const ASTVec &vec);
-
-    friend ostream &operator<<(ostream &os, const ASTNode &node) { 
-      node.LispPrint(os, 0); 
-      return os; 
-    };
-    
-    // Check whether the ASTNode points to anything.  Undefined nodes
-    // are created by the default constructor.  In binding table (for
-    // lambda args, etc.), undefined nodes are used to represent
-    // deleted entries.
-    bool IsDefined() const { return _int_node_ptr != NULL; }        
-
-    /* Hasher class for STL hash_maps and hash_sets that use ASTNodes
-     * as keys.  Needs to be public so people can define hash tables
-     * (and use ASTNodeMap class)*/
-    class ASTNodeHasher {
-    public:
-      size_t operator() (const ASTNode& n) const{ 
-	return (size_t) n._int_node_ptr; 
-	//return (size_t)n.GetNodeNum();
-      };
-    }; //End of ASTNodeHasher
-  
-    /* Equality for ASTNode hash_set and hash_map. Returns true iff
-     * internal pointers are the same.  Needs to be public so people
-     * can define hash tables (and use ASTNodeSet class)*/
-    class ASTNodeEqual {
-    public:
-      bool operator()(const ASTNode& n1, const ASTNode& n2) const{ 
-	return (n1._int_node_ptr == n2._int_node_ptr); 
-      }
-    }; //End of ASTNodeEqual
-  }; //End of Class ASTNode
-
-  void FatalError(const char * str, const ASTNode& a, int w = 0);
-  void FatalError(const char * str);
-  void SortByExprNum(ASTVec& c);
-  bool exprless(const ASTNode n1, const ASTNode n2);
-  bool isAtomic(Kind k);
-
-  /***************************************************************************/
-  /*  Class ASTInternal:Abstract base class for internal node representation.*/
-  /*                    Requires Kind and ChildNodes so same traversal works */
-  /*                    on all nodes.                                        */
-  /***************************************************************************/
-  class ASTInternal {
-
-    friend class ASTNode;
-
-  protected:    
-
-    // reference count.
-    int _ref_count;
-
-    // Kind.  It's a type tag and the operator.
-    Kind _kind;  
-
-    // The vector of children (*** should this be in ASTInterior? ***)
-    ASTVec _children;
-
-    // Manager object.  Having this backpointer means it's easy to
-    // find the manager when we need it.
-    BeevMgr &_bm;
-
-    //Nodenum is a unique positive integer for the node.  The nodenum
-    //of a node should always be greater than its descendents (which
-    //is easily achieved by incrementing the number each time a new
-    //node is created).
-    int _node_num;
-
-    // Length of bitvector type for array index.  The term is an
-    // array iff this is positive.  Otherwise, the term is a bitvector
-    // or a bit.
-    unsigned int _index_width;
-
-    // Length of bitvector type for scalar value or array element.
-    // If this is one, the term represents a single bit (same as a bitvector
-    // of length 1).  It must be 1 or greater.
-    unsigned int _value_width;
-
-    // Increment refcount.
-#ifndef SMTLIB
-    void IncRef() { ++_ref_count; }
-#else
-    void IncRef() { }
-#endif
-
-    // DecRef is a potentially expensive, because it has to delete 
-    // the node from the unique table, in addition to freeing it.
-    // FIXME:  Consider putting in a backpointer (iterator) to the hash
-    // table entry so it can be deleted without looking it up again.
-    void DecRef();
-
-    virtual Kind GetKind() const { return _kind; }
-
-    virtual ASTVec const &GetChildren() const { return _children; }
-
-    int GetNodeNum() const { return _node_num; }
-
-    void SetNodeNum(int nn) { _node_num = nn; };
-
-    // Constructor (bm only)
-    ASTInternal(BeevMgr &bm, int nodenum = 0) :
-      _ref_count(0),
-      _kind(UNDEFINED),
-      _bm(bm),
-      _node_num(nodenum),
-      _index_width(0),
-      _value_width(0) { }
-
-    // Constructor (kind only, empty children, int nodenum) 
-    ASTInternal(Kind kind, BeevMgr &bm, int nodenum = 0) : 
-      _ref_count(0),
-      _kind(kind),
-      _bm(bm),
-      _node_num(nodenum),
-      _index_width(0),
-      _value_width(0) { } 
-
-    // Constructor (kind and children).  This copies the contents of
-    // the child nodes.
-    // FIXME: is there a way to avoid repeating these?
-    ASTInternal(Kind kind, const ASTVec &children, BeevMgr &bm, int nodenum = 0) : 
-      _ref_count(0),
-      _kind(kind),
-      _children(children),
-      _bm(bm),
-      _node_num(nodenum),
-      _index_width(0),
-      _value_width(0) { } 
-
-    // Copy constructor.  This copies the contents of the child nodes
-    // array, along with everything else.  Assigning the smart pointer,
-    // ASTNode, does NOT invoke this; This should only be used for 
-    // temporary hash keys before uniquefication.
-    // FIXME:  I don't think children need to be copied.
-    ASTInternal(const ASTInternal &int_node, int nodenum = 0) :
-      _ref_count(0),
-      _kind(int_node._kind),
-      _children(int_node._children),
-      _bm(int_node._bm),
-      _node_num(int_node._node_num), 
-      _index_width(int_node._index_width),
-      _value_width(int_node._value_width) { } 
-
-    // Copying assign operator.  Also copies contents of children.
-    ASTInternal& operator=(const ASTInternal &int_node);
-
-    // Cleanup function for removing from hash table
-    virtual void CleanUp() = 0;
-
-    // Destructor (does nothing, but is declared virtual here.
-    virtual ~ASTInternal();
-
-    // Abstract virtual print function for internal node.
-    virtual void nodeprint(ostream& os) { os << "*"; };
-  }; //End of Class ASTInternal
-
-  // FIXME: Should children be only in interior node type?
-  /***************************************************************************
-    Class ASTInterior: Internal representation of an interior
-       ASTNode.  Generally, these nodes should have at least one
-      child
-  ***************************************************************************/
-  class ASTInterior : public ASTInternal {    
-
-    friend class BeevMgr;
-    friend class ASTNodeHasher;
-    friend class ASTNodeEqual;   
-
-  private:
-
-    // Hasher for ASTInterior pointer nodes
-    class ASTInteriorHasher {
-    public:
-      size_t operator()(const ASTInterior *int_node_ptr) const;
-    };
-
-    // Equality for ASTInterior nodes
-    class ASTInteriorEqual {
-    public:
-      bool operator()(const ASTInterior *int_node_ptr1, 
-		      const ASTInterior *int_node_ptr2) const{
-	return (*int_node_ptr1 == *int_node_ptr2);
-      }
-    };
-
-    // Used in Equality class for hash tables
-    friend bool operator==(const ASTInterior &int_node1, 
-			   const ASTInterior &int_node2){
-      return (int_node1._kind == int_node2._kind) && 
-	(int_node1._children == int_node2._children);
-    }
-
-    // Call this when deleting a node that has been stored in the
-    // the unique table
-    virtual void CleanUp();
-
-    // Returns kinds.  "lispprinter" handles printing of parenthesis
-    // and childnodes.
-    virtual void nodeprint(ostream& os) {
-      os << _kind_names[_kind];
-    }
-    public:
-
-    // FIXME: This should not be public, but has to be because the
-    // ASTInterior hash table insists on it.  I can't seem to make the
-    // private destructor visible to hash_set.  It does not even work
-    // to put "friend class hash_set<ASTInterior, ...>" in here.
-
-    // Basic constructors
-    ASTInterior(Kind kind,  BeevMgr &bm) :
-      ASTInternal(kind, bm) {  }    
-
-    ASTInterior(Kind kind, ASTVec &children, BeevMgr &bm) :
-      ASTInternal(kind, children, bm) {  }    
-
-    //Copy constructor.  This copies the contents of the child nodes
-    //array, along with everything else. Assigning the smart pointer,
-    //ASTNode, does NOT invoke this.
-    ASTInterior(const ASTInterior &int_node) : ASTInternal(int_node) { }
-
-    // Destructor (does nothing, but is declared virtual here.
-    virtual ~ASTInterior();
-
-  }; //End of ASTNodeInterior
-
-
-  /***************************************************************************/
-  /*  Class ASTSymbol:  Class to represent internals of Symbol node.         */
-  /***************************************************************************/
-  class ASTSymbol : public ASTInternal{
-    friend class BeevMgr;
-    friend class ASTNode;
-    friend class ASTNodeHasher;
-    friend class ASTNodeEqual;
-
-  private:
-    // The name of the symbol
-    const char * const _name;
-    
-    class ASTSymbolHasher{
-    public:
-      size_t operator() (const ASTSymbol *sym_ptr) const{ 
-	hash<char*> h; 
-	return h(sym_ptr->_name); 
-      };
-    };
-
-    // Equality for ASTInternal nodes
-    class ASTSymbolEqual{
-    public:
-      bool operator()(const ASTSymbol *sym_ptr1, const ASTSymbol *sym_ptr2) const{ 
-	return (*sym_ptr1 == *sym_ptr2); 
-      }
-    };
-
-    friend bool operator==(const ASTSymbol &sym1, const ASTSymbol &sym2){
-      return (strcmp(sym1._name, sym2._name) == 0);
-    }
-
-    const char *GetName() const{return _name;}  
-
-    // Print function for symbol -- return name */
-    virtual void nodeprint(ostream& os) { os << _name;}
-
-    // Call this when deleting a node that has been stored in the
-    // the unique table
-    virtual void CleanUp();
-
-    public:
-
-    // Default constructor
-    ASTSymbol(BeevMgr &bm) : ASTInternal(bm), _name(NULL) { }
-
-    // Constructor.  This does NOT copy its argument.
-    ASTSymbol(const char * const name, BeevMgr &bm) : ASTInternal(SYMBOL, bm), 
-						      _name(name) { }
-    
-    // Destructor (does nothing, but is declared virtual here.
-    virtual ~ASTSymbol();
-    
-    // Copy constructor
-    // FIXME: seems to be calling default constructor for astinternal
-    ASTSymbol(const ASTSymbol &sym) :
-      ASTInternal(sym._kind, sym._children, sym._bm), 
-      _name(sym._name) { } 
-  }; //End of ASTSymbol
-  
-
-  /***************************************************************************/
-  /*  Class ASTBVConst:  Class to represent internals of a bitvectorconst    */
-  /***************************************************************************/
-
-#ifndef NATIVE_C_ARITH
-
-  class ASTBVConst : public ASTInternal {
-    friend class BeevMgr;
-    friend class ASTNode;
-    friend class ASTNodeHasher;
-    friend class ASTNodeEqual;
-    
-  private:
-    //This is the private copy of a bvconst currently
-    //This should not be changed at any point
-    CBV _bvconst;
-
-    class ASTBVConstHasher{
-    public:
-      size_t operator() (const ASTBVConst * bvc) const {
-        return CONSTANTBV::BitVector_Hash(bvc->_bvconst);
-      };
-    };
-
-    class ASTBVConstEqual{
-    public:
-      bool operator()(const ASTBVConst * bvc1, const ASTBVConst  * bvc2) const { 
-        if( bvc1->_value_width != bvc2->_value_width){
-	  return false;
-	}  
-	return (0==CONSTANTBV::BitVector_Compare(bvc1->_bvconst,bvc2->_bvconst));
-      }
-    };
-    
-    //FIXME Keep an eye on this function
-    ASTBVConst(CBV bv, unsigned int width, BeevMgr &bm) :
-      ASTInternal(BVCONST, bm)
-    {
-      _bvconst = CONSTANTBV::BitVector_Clone(bv);
-      _value_width = width;
-    }
-
-    friend bool operator==(const ASTBVConst &bvc1, const ASTBVConst &bvc2){
-      if(bvc1._value_width != bvc2._value_width)
-        return false;
-      return (0==CONSTANTBV::BitVector_Compare(bvc1._bvconst,bvc2._bvconst));
-    }
-    // Call this when deleting a node that has been stored in the
-    // the unique table
-    virtual void CleanUp();
-
-    // Print function for bvconst -- return _bvconst value in bin format
-    virtual void nodeprint(ostream& os) {
-      unsigned char *res;
-      const char *prefix;
-
-      if (_value_width%4 == 0) {
-        res = CONSTANTBV::BitVector_to_Hex(_bvconst);
-        prefix = "0hex";
-      } else {      
-        res = CONSTANTBV::BitVector_to_Bin(_bvconst);
-        prefix = "0bin";
-      }
-      if (NULL == res) {
-        os << "nodeprint: BVCONST : could not convert to string" << _bvconst;
-        FatalError("");
-      }
-      os << prefix << res;
-      CONSTANTBV::BitVector_Dispose(res);
-    }
-
-    // Copy constructor.     
-    ASTBVConst(const ASTBVConst &sym) : 
-      ASTInternal(sym._kind, sym._children, sym._bm)
-    {
-      _bvconst = CONSTANTBV::BitVector_Clone(sym._bvconst);
-      _value_width = sym._value_width;
-    }
-    
-  public:
-    virtual ~ASTBVConst(){
-       CONSTANTBV::BitVector_Destroy(_bvconst);
-    }
-
-    CBV GetBVConst() const {return _bvconst;}
-  }; //End of ASTBVConst
-
-  //FIXME This function is DEPRICATED
-  //Do not use in the future
-  inline unsigned int GetUnsignedConst(const ASTNode n) {
-    if(32 < n.GetValueWidth())
-      FatalError("GetUnsignedConst: cannot convert bvconst of length greater than 32 to unsigned int:");
-        
-    return (unsigned int) *((unsigned int *)n.GetBVConst());
-  }
-#else
-  class ASTBVConst : public ASTInternal {
-    friend class BeevMgr;
-    friend class ASTNode;
-    friend class ASTNodeHasher;
-    friend class ASTNodeEqual;
-
-  private:
-    // the bitvector contents. bitvector contents will be in two
-    // modes. one mode where all bitvectors are NATIVE and in this
-    // mode we use native unsigned long long int to represent the
-    // 32/64 bitvectors. The other for arbitrary length bitvector
-    // operations.
-    const unsigned long long int _bvconst;
-
-    class ASTBVConstHasher{
-    public:
-      size_t operator() (const ASTBVConst * bvc) const{ 
-	//Thomas Wang's 64 bit Mix Function
-	unsigned long long int key(bvc->_bvconst);
-	key += ~(key << 32);
-	key ^= (key  >> 22);
-	key += ~(key << 13);
-	key ^= (key  >> 8);
-	key += (key  << 3);
-	key ^= (key  >> 15);
-	key += ~(key << 27);
-	key ^= (key  >> 31);
-	
-	size_t return_key = key;
-	return return_key;
-      };
-    };
-
-    class ASTBVConstEqual{
-    public:
-      bool operator()(const ASTBVConst * bvc1, const ASTBVConst  * bvc2) const { 
-	return ((bvc1->_bvconst == bvc2->_bvconst) 
-		&& (bvc1->_value_width == bvc2->_value_width));
-      }
-    };
-
-    // Call this when deleting a node that has been stored in the
-    // the unique table
-    virtual void CleanUp();
-  public:
-    // Default constructor
-    ASTBVConst(const unsigned long long int bv, BeevMgr &bm) : 
-      ASTInternal(BVCONST, bm), _bvconst(bv) { 
-    }
-
-    // Copy constructor. FIXME: figure out how this is supposed to
-    // work.
-    ASTBVConst(const ASTBVConst &sym) : 
-      ASTInternal(sym._kind, sym._children, sym._bm), 
-      _bvconst(sym._bvconst) { 
-      _value_width = sym._value_width;
-    } 
-
-    // Destructor (does nothing, but is declared virtual here)
-    virtual ~ASTBVConst() { } 
-    
-    friend bool operator==(const ASTBVConst &sym1, const ASTBVConst &sym2){
-      return ((sym1._bvconst == sym2._bvconst) && 
-	      (sym1._value_width == sym2._value_width));
-    }
-
-    // Print function for bvconst -- return _bvconst value in binary format
-    virtual void nodeprint(ostream& os) {
-      string s = "0bin";
-      unsigned long long int bitmask = 0x8000000000000000LL;
-      bitmask = bitmask >> (64-_value_width);
-
-      for (; bitmask > 0; bitmask >>= 1)
-	s += (_bvconst & bitmask) ? '1' : '0';	
-      os << s;
-    }
-    
-    unsigned long long int GetBVConst() const  {return _bvconst;}
-  }; //End of ASTBVConst
-
-  //return value of bvconst
-  inline unsigned int GetUnsignedConst(const ASTNode n) {
-    if(32 < n.GetValueWidth())
-      FatalError("GetUnsignedConst: cannot convert bvconst of length greater than 32 to unsigned int:");    
-    return (unsigned int)n.GetBVConst();
-  }
-#endif
-/*
-#else
-  // the bitvector contents. bitvector contents will be in two
-  // modes. one mode where all bitvectors are NATIVE and in this mode
-  // we use native unsigned long long int to represent the 32/64
-  // bitvectors. The other for arbitrary length bitvector operations.
-
-  //BVCONST defined for arbitrary length bitvectors
-  class ASTBVConst : public ASTInternal{
-    friend class BeevMgr;
-    friend class ASTNode;
-    friend class ASTNodeHasher;
-    friend class ASTNodeEqual;
-
-  private:
-    const char * const _bvconst;
-
-    class ASTBVConstHasher{
-    public:
-      size_t operator() (const ASTBVConst * bvc) const{ 
-	hash<char*> h;	
-	return h(bvc->_bvconst);
-      };
-    };
-
-    class ASTBVConstEqual{
-    public:
-      bool operator()(const ASTBVConst * bvc1, const ASTBVConst  * bvc2) const { 
-	if(bvc1->_value_width != bvc2->_value_width)
-	  return false;
-	return (0 == strncmp(bvc1->_bvconst,bvc2->_bvconst,bvc1->_value_width));
-      }
-    };
-    
-    ASTBVConst(const char * bv, BeevMgr &bm) : 
-      ASTInternal(BVCONST, bm), _bvconst(bv) { 
-      //_value_width = strlen(bv);
-    }
-
-    friend bool operator==(const ASTBVConst &bvc1, const ASTBVConst &bvc2){
-      if(bvc1._value_width != bvc2._value_width)
-	return false;
-      return (0 == strncmp(bvc1._bvconst,bvc2._bvconst,bvc1._value_width));
-    }
-
-    // Call this when deleting a node that has been stored in the
-    // the unique table
-    virtual void CleanUp();
-
-    // Print function for bvconst -- return _bvconst value in binary format
-    virtual void nodeprint(ostream& os) {
-      if(_value_width%4 == 0) {
-	unsigned int *  iii = CONSTANTBV::BitVector_Create(_value_width,true);
-	CONSTANTBV::ErrCode e = CONSTANTBV::BitVector_from_Bin(iii,(unsigned char*)_bvconst);
-	//error printing
-	if(0 != e) {
-	  os << "nodeprint: BVCONST : wrong hex value: " << BitVector_Error(e);
-	  FatalError("");
-	}
-	unsigned char * ccc = CONSTANTBV::BitVector_to_Hex(iii);
-	os << "0hex" << ccc;
-	CONSTANTBV::BitVector_Destroy(iii);
-      }
-      else {
-	std::string s(_bvconst,_value_width);
-	s = "0bin" + s;
-	os << s;
-      }
-    }
-
-    // Copy constructor.     
-    ASTBVConst(const ASTBVConst &sym) : ASTInternal(sym._kind, sym._children, sym._bm),_bvconst(sym._bvconst) { 
-      //checking if the input is in the correct format
-      for(unsigned int jj=0;jj<sym._value_width;jj++)
-	if(!(sym._bvconst[jj] == '0' || sym._bvconst[jj] == '1')) {
-	  cerr << "Fatal Error: wrong input to ASTBVConst copy constructor:" << sym._bvconst << endl;
-	  FatalError("");
-	}
-      _value_width = sym._value_width;
-    } 
-  public:
-    // Destructor (does nothing, but is declared virtual here)
-    virtual ~ASTBVConst(){}
-
-    const char * const GetBVConst() const {return _bvconst;}
-  }; //End of ASTBVConst
-
-  unsigned int * ConvertToCONSTANTBV(const char * s);
-
-  //return value of bvconst
-  inline unsigned int GetUnsignedConst(const ASTNode n) {
-    if(32 < n.GetValueWidth())
-      FatalError("GetUnsignedConst: cannot convert bvconst of length greater than 32 to unsigned int:");    
-    std::string s(n.GetBVConst(), n.GetValueWidth());
-      unsigned int output = strtoul(s.c_str(),NULL,2);
-      return output;
-  } //end of ASTBVConst class
-#endif
-*/
-  /***************************************************************************
-   * Typedef ASTNodeMap:  This is a hash table from ASTNodes to ASTNodes.
-   * It is very convenient for attributes that are not speed-critical
-   **************************************************************************/
-  // These are generally useful for storing ASTNodes or attributes thereof
-  // Hash table from ASTNodes to ASTNodes
-  typedef hash_map<ASTNode, ASTNode, 
-		   ASTNode::ASTNodeHasher, 
-		   ASTNode::ASTNodeEqual> ASTNodeMap;
-
-  // Function to dump contents of ASTNodeMap
-  ostream &operator<<(ostream &os, const ASTNodeMap &nmap);
-  
-  /***************************************************************************
-   Typedef ASTNodeSet:  This is a hash set of ASTNodes.  Very useful
-   for representing things like "visited nodes"
-  ***************************************************************************/
-  typedef hash_set<ASTNode, 
-		   ASTNode::ASTNodeHasher, 
-		   ASTNode::ASTNodeEqual> ASTNodeSet;
-
-  typedef hash_multiset<ASTNode, 
-			ASTNode::ASTNodeHasher, 
-			ASTNode::ASTNodeEqual> ASTNodeMultiSet;
-
-  //external parser table for declared symbols.
-  //FIXME: move to a more appropriate place
-  extern ASTNodeSet _parser_symbol_table;
-  
-  /***************************************************************************
-    Class LispPrinter:  iomanipulator for printing ASTNode or ASTVec       
-  ***************************************************************************/
-  class LispPrinter {
-
-  public:
-    ASTNode _node;
-
-    // number of spaces to print before first real character of
-    // object.
-    int _indentation;  
-
-    // FIXME: pass ASTNode by reference
-    // Constructor to build the LispPrinter object
-    LispPrinter(ASTNode node, int indentation): _node(node), _indentation(indentation) { }    
-
-    friend ostream &operator<<(ostream &os, const LispPrinter &lp){ 
-      return lp._node.LispPrint(os, lp._indentation); 
-    };
-
-  }; //End of ListPrinter
-  
-  //This is the IO manipulator.  It builds an object of class
-  //"LispPrinter" that has a special overloaded "<<" operator.
-  inline LispPrinter lisp(const ASTNode &node, int indentation = 0){
-    LispPrinter lp(node, indentation);
-    return lp;
-  }
-  
-  /***************************************************************************/
-  /*  Class LispVecPrinter:iomanipulator for printing vector of ASTNodes     */
-  /***************************************************************************/
-  class LispVecPrinter {
-
-  public:
-    const ASTVec * _vec;
-    // number of spaces to print before first real
-    // character of object.    
-    int _indentation;
-    
-    // Constructor to build the LispPrinter object
-    LispVecPrinter(const ASTVec &vec, int indentation){
-      _vec = &vec; _indentation = indentation; 
-    }
-    
-    friend ostream &operator<<(ostream &os, const LispVecPrinter &lvp){
-    LispPrintVec(os, *lvp._vec, lvp._indentation);
-    return os;
-    };
-  }; //End of Class ListVecPrinter
-
-  //iomanipulator. builds an object of class "LisPrinter" that has a
-  //special overloaded "<<" operator.
-  inline LispVecPrinter lisp(const ASTVec &vec, int indentation = 0){
-    LispVecPrinter lvp(vec, indentation);
-    return lvp;
-  }
-
-
-  /*****************************************************************
-   * INLINE METHODS from various classed, declared here because of
-   * dependencies on classes that are declared later.
-   *****************************************************************/
-  // ASTNode accessor function.
-  inline Kind ASTNode::GetKind() const { 
-    //cout << "GetKind: " << _int_node_ptr; 
-    return _int_node_ptr->GetKind(); 
-  }
-
-  // FIXME: should be const ASTVec const?  
-  // Declared here because of same ordering problem as  GetKind.
-  inline const ASTVec &ASTNode::GetChildren() const { 
-    return _int_node_ptr->GetChildren(); 
-  }
-
-  // Access node number
-  inline int ASTNode::GetNodeNum() const { 
-    return _int_node_ptr->_node_num; 
-  }
-
-  inline unsigned int ASTNode::GetIndexWidth () const { 
-    return _int_node_ptr->_index_width; 
-  }
-  
-  inline void ASTNode::SetIndexWidth (unsigned int iw) const { 
-    _int_node_ptr->_index_width = iw;
-  }
-  
-  inline unsigned int ASTNode::GetValueWidth () const { 
-    return _int_node_ptr->_value_width; 
-  }
-  
-  inline void ASTNode::SetValueWidth (unsigned int vw) const {
-    _int_node_ptr->_value_width = vw; 
-  }
-
-  //return the type of the ASTNode: 0 iff BOOLEAN; 1 iff BITVECTOR; 2
-  //iff ARRAY; 3 iff UNKNOWN;
-  inline types ASTNode::GetType() const {
-    if((GetIndexWidth() == 0) && (GetValueWidth() == 0)) //BOOLEAN
-      return BOOLEAN_TYPE;
-    if((GetIndexWidth() == 0) && (GetValueWidth() > 0))  //BITVECTOR
-      return BITVECTOR_TYPE;
-    if((GetIndexWidth() > 0) && (GetValueWidth() > 0)) //ARRAY
-      return ARRAY_TYPE;
-    return UNKNOWN_TYPE; 
-  }
-
-  // Constructor; creates a new pointer, increments refcount of
-  // pointed-to object.
-#ifndef SMTLIB
-  inline ASTNode::ASTNode(ASTInternal *in) : _int_node_ptr(in) { 
-    if (in) in->IncRef(); 
-  }
-#else
-  inline ASTNode::ASTNode(ASTInternal *in) : _int_node_ptr(in) { };
-#endif
-
-  // Assignment.  Increment refcount of new value, decrement refcount
-  // of old value and destroy if this was the last pointer.  FIXME:
-  // accelerate this by creating an intnode with a ref counter instead
-  // of pointing to NULL.  Need a special check in CleanUp to make
-  // sure the null node never gets freed.
-
-#ifndef SMTLIB
-  inline ASTNode& ASTNode::operator=(const ASTNode& n) {
-    if (n._int_node_ptr) {
-      n._int_node_ptr->IncRef();
-    }
-    if (_int_node_ptr) {
-      _int_node_ptr->DecRef();
-    }
-    _int_node_ptr = n._int_node_ptr;
-    return *this;
-  }
-#else
-  inline ASTNode& ASTNode::operator=(const ASTNode& n) {
-    _int_node_ptr = n._int_node_ptr;
-    return *this;
-  }
-#endif
-
-#ifndef SMTLIB
-  inline void ASTInternal::DecRef()
-  {
-    if (--_ref_count == 0) {
-      // Delete node from unique table and kill it.
-      CleanUp();
-    }
-  }
-
-  // Destructor
-  inline ASTNode::~ASTNode()
-  {
-    if (_int_node_ptr) {
-      _int_node_ptr->DecRef();
-    }
-  }
-#else
-  // No refcounting
-  inline void ASTInternal::DecRef()
-  {
-  }
-
-  // Destructor
-  inline ASTNode::~ASTNode()
-  {
-  };
-#endif
-
-  inline BeevMgr& ASTNode::GetBeevMgr() const { return _int_node_ptr->_bm; }
-
-  /***************************************************************************
-   * Class BeevMgr.  This holds all "global" variables for the system, such as
-   * unique tables for the various kinds of nodes.
-   ***************************************************************************/
-  class BeevMgr {
-    friend class ASTNode;	// ASTNode modifies AlreadyPrintedSet
-				// in BeevMgr
-    friend class ASTInterior;
-    friend class ASTBVConst;
-    friend class ASTSymbol;
-
-    // FIXME: The values appear to be the same regardless of the value of SMTLIB
-    // initial hash table sizes, to save time on resizing.
-#ifdef SMTLIB
-    static const int INITIAL_INTERIOR_UNIQUE_TABLE_SIZE = 100;
-    static const int INITIAL_SYMBOL_UNIQUE_TABLE_SIZE = 100;
-    static const int INITIAL_BVCONST_UNIQUE_TABLE_SIZE = 100;
-    static const int INITIAL_BBTERM_MEMO_TABLE_SIZE = 100;
-    static const int INITIAL_BBFORM_MEMO_TABLE_SIZE = 100;
-
-    static const int INITIAL_SIMPLIFY_MAP_SIZE = 100;
-    static const int INITIAL_SOLVER_MAP_SIZE = 100;
-    static const int INITIAL_ARRAYREAD_SYMBOL_SIZE = 100;
-    static const int INITIAL_INTRODUCED_SYMBOLS_SIZE = 100;
-#else
-    // these are the STL defaults
-    static const int INITIAL_INTERIOR_UNIQUE_TABLE_SIZE = 100;
-    static const int INITIAL_SYMBOL_UNIQUE_TABLE_SIZE = 100;
-    static const int INITIAL_BVCONST_UNIQUE_TABLE_SIZE = 100;
-    static const int INITIAL_BBTERM_MEMO_TABLE_SIZE = 100;
-    static const int INITIAL_BBFORM_MEMO_TABLE_SIZE = 100;
-
-    static const int INITIAL_SIMPLIFY_MAP_SIZE = 100;
-    static const int INITIAL_SOLVER_MAP_SIZE = 100;
-    static const int INITIAL_ARRAYREAD_SYMBOL_SIZE = 100;
-    static const int INITIAL_INTRODUCED_SYMBOLS_SIZE = 100;
-#endif
-
-  private:
-    // Typedef for unique Interior node table. 
-    typedef hash_set<ASTInterior *, 
-		     ASTInterior::ASTInteriorHasher, 
-		     ASTInterior::ASTInteriorEqual> ASTInteriorSet;
-
-    // Typedef for unique Symbol node (leaf) table.
-    typedef hash_set<ASTSymbol *, 
-		     ASTSymbol::ASTSymbolHasher, 
-		     ASTSymbol::ASTSymbolEqual> ASTSymbolSet;
-
-    // Unique tables to share nodes whenever possible.
-    ASTInteriorSet _interior_unique_table;
-    //The _symbol_unique_table is also the symbol table to be used
-    //during parsing/semantic analysis
-    ASTSymbolSet _symbol_unique_table;
-    
-    //Typedef for unique BVConst node (leaf) table.
-    typedef hash_set<ASTBVConst *, 
-		     ASTBVConst::ASTBVConstHasher,
-		     ASTBVConst::ASTBVConstEqual> ASTBVConstSet;
-
-    //table to uniquefy bvconst
-    ASTBVConstSet _bvconst_unique_table;
-
-    // type of memo table.
-    typedef hash_map<ASTNode, ASTVec,
-		     ASTNode::ASTNodeHasher, 
-		     ASTNode::ASTNodeEqual> ASTNodeToVecMap;
-
-    typedef hash_map<ASTNode,ASTNodeSet,
-		     ASTNode::ASTNodeHasher,
-		     ASTNode::ASTNodeEqual> ASTNodeToSetMap;
-    
-    // Memo table for bit blasted terms.  If a node has already been
-    // bitblasted, it is mapped to a vector of Boolean formulas for
-    // the bits.
-    
-    //OLD: ASTNodeToVecMap BBTermMemo;
-    ASTNodeMap BBTermMemo;
-    
-    // Memo table for bit blasted formulas.  If a node has already
-    // been bitblasted, it is mapped to a node representing the
-    // bitblasted equivalent
-    ASTNodeMap BBFormMemo;
-    
-    //public:
-    // Get vector of Boolean formulas for sum of two
-    // vectors of Boolean formulas
-    void BBPlus2(ASTVec& sum, const ASTVec& y, ASTNode cin);
-    // Increment
-    ASTVec BBInc(ASTVec& x);
-    // Add one bit to a vector of bits.
-    ASTVec BBAddOneBit(ASTVec& x, ASTNode cin);
-    // Bitwise complement
-    ASTVec BBNeg(const ASTVec& x);
-    // Unary minus
-    ASTVec BBUminus(const ASTVec& x);
-    // Multiply.
-    ASTVec BBMult(const ASTVec& x, const ASTVec& y);
-    // AND each bit of vector y with single bit b and return the result.
-    // (used in BBMult)
-    ASTVec BBAndBit(const ASTVec& y, ASTNode b);
-    // Returns ASTVec for result - y.  This destroys "result".
-    void BBSub(ASTVec& result, const ASTVec& y);
-    // build ITE's (ITE cond then[i] else[i]) for each i.
-    ASTVec BBITE(const ASTNode& cond, 
-		 const ASTVec& thn, const ASTVec& els);
-    // Build a vector of zeros.
-    ASTVec BBfill(unsigned int width, ASTNode fillval);
-    // build an EQ formula
-    ASTNode BBEQ(const ASTVec& left, const ASTVec& right);
-
-    // This implements a variant of binary long division.
-    // q and r are "out" parameters.  rwidth puts a bound on the
-    // recursion depth.   Unsigned only, for now.
-    void BBDivMod(const ASTVec &y,
-		  const ASTVec &x,
-		  ASTVec &q,
-		  ASTVec &r,
-		  unsigned int rwidth);
-    
-    // Return formula for majority function of three formulas.
-    ASTNode Majority(const ASTNode& a, const ASTNode& b, const ASTNode& c);
-
-    // Internal bit blasting routines.
-    ASTNode BBBVLE(const ASTVec& x, const ASTVec& y, bool is_signed);
-
-    // Return bit-blasted form for BVLE, BVGE, BVGT, SBLE, etc. 
-    ASTNode BBcompare(const ASTNode& form);
-
-    // Left and right shift one.  Writes into x.
-    void BBLShift(ASTVec& x);
-    void BBRShift(ASTVec& x);
-
-  public:
-    // Simplifying create functions
-    ASTNode CreateSimpForm(Kind kind, ASTVec &children);
-    ASTNode CreateSimpForm(Kind kind, const ASTNode& child0);
-    ASTNode CreateSimpForm(Kind kind,
-				    const ASTNode& child0,
-				    const ASTNode& child1);
-    ASTNode CreateSimpForm(Kind kind,
-				    const ASTNode& child0,
-				    const ASTNode& child1,
-				    const ASTNode& child2);
-
-    ASTNode CreateSimpNot(const ASTNode& form);
-
-    // These are for internal use only.
-    // FIXME: Find a way to make this local to SimpBool, so they're
-    // not in AST.h
-    ASTNode CreateSimpXor(const ASTNode& form1,
-			  const ASTNode& form2);
-    ASTNode CreateSimpXor(ASTVec &children);
-    ASTNode CreateSimpAndOr(bool isAnd,
-				     const ASTNode& form1,
-				     const ASTNode& form2);
-    ASTNode CreateSimpAndOr(bool IsAnd, ASTVec &children);
-    ASTNode CreateSimpFormITE(const ASTNode& child0,
-				       const ASTNode& child1,
-				       const ASTNode& child2);
-    
-
-    // Declarations of BitBlaster functions (BitBlast.cpp)
-  public:
-    // Adds or removes a NOT as necessary to negate a literal.
-    ASTNode Negate(const ASTNode& form);
-
-    // Bit blast a bitvector term.  The term must have a kind for a
-    // bitvector term.  Result is a ref to a vector of formula nodes
-    // representing the boolean formula.
-    const ASTNode BBTerm(const ASTNode& term);
-
-    const ASTNode BBForm(const ASTNode& formula);
-
-    // Declarations of CNF conversion (ToCNF.cpp)
-  public:
-    // ToCNF converts a bit-blasted Boolean formula to Conjunctive
-    // 	Normal Form, suitable for many SAT solvers.  Our CNF representation
-    // 	is an STL vector of STL vectors, for independence from any particular
-    // 	SAT solver's representation.  There needs to be a separate driver to
-    // 	convert our clauselist to the representation used by the SAT solver.    
-    // 	Currently, there is only one such solver and its driver is "ToSAT"
-    
-    // Datatype for clauses
-    typedef ASTVec * ClausePtr;
-    
-    // Datatype for Clauselists
-    typedef vector<ClausePtr> ClauseList;
-
-    // Convert a Boolean formula to an equisatisfiable CNF formula.
-    ClauseList *ToCNF(const ASTNode& form);
-
-    // Print function for debugging
-    void PrintClauseList(ostream& os, ClauseList& cll); 
-
-    // Free the clause list and all its clauses.
-    void DeleteClauseList(BeevMgr::ClauseList *cllp);
-
-    // Map from formulas to representative literals, for debugging.
-    ASTNodeMap RepLitMap;
-
-  private:
-    // Global for assigning new node numbers.
-    int _max_node_num;
-    
-    const ASTNode ASTFalse, ASTTrue, ASTUndefined;
-    
-    // I just did this so I could put it in as a fake return value in
-    // methods that return a ASTNode &, to make -Wall shut up.
-    ASTNode dummy_node;
-
-    //BeevMgr Constructor, Destructor and other misc. functions
-  public:
-
-    int NewNodeNum() { _max_node_num += 2; return _max_node_num; } 
-    
-    // Table for DAG printing.
-    ASTNodeSet AlreadyPrintedSet;
-
-    //Tables for Presentation language printing
-
-    //Nodes seen so far
-    ASTNodeSet PLPrintNodeSet;
-
-    //Map from ASTNodes to LetVars
-    ASTNodeMap NodeLetVarMap;
-    
-    //This is a vector which stores the Node to LetVars pairs. It
-    //allows for sorted printing, as opposed to NodeLetVarMap
-    std::vector<pair<ASTNode,ASTNode> > NodeLetVarVec;
-
-    //a partial Map from ASTNodes to LetVars. Needed in order to
-    //correctly print shared subterms inside the LET itself
-    ASTNodeMap NodeLetVarMap1;
-
-    //functions to lookup nodes from the memo tables. these should be
-    //private.
-  private:
-    //Destructively appends back_child nodes to front_child nodes.
-    //If back_child nodes is NULL, no appending is done.  back_child
-    //nodes are not modified.  Then it returns the hashed copy of the
-    //node, which is created if necessary.
-    ASTInterior *CreateInteriorNode(Kind kind,
-				    ASTInterior *new_node,
-				    // this is destructively modified.
-				    const ASTVec & back_children = _empty_ASTVec);
-
-    // Create unique ASTInterior node.
-    ASTInterior *LookupOrCreateInterior(ASTInterior *n);
-
-    // Create unique ASTSymbol node. 
-    ASTSymbol *LookupOrCreateSymbol(ASTSymbol& s);
-    
-    // Called whenever we want to make sure that the Symbol is
-    // declared during semantic analysis
-    bool LookupSymbol(ASTSymbol& s);
-      
-    // Called by ASTNode constructors to uniqueify ASTBVConst
-    ASTBVConst *LookupOrCreateBVConst(ASTBVConst& s);
-
-    //Public functions for CreateNodes and Createterms
-  public:
-    // Create and return an ASTNode for a symbol
-    ASTNode CreateSymbol(const char * const name);
-
-    // Create and return an ASTNode for a symbol
-    // Width is number of bits.
-    ASTNode CreateBVConst(unsigned int width, unsigned long long int bvconst);
-    ASTNode CreateZeroConst(unsigned int width);
-    ASTNode CreateOneConst(unsigned int width);
-    ASTNode CreateTwoConst(unsigned int width);
-    ASTNode CreateMaxConst(unsigned int width);
-
-    // Create and return an ASTNode for a symbol
-    // Optional base was a problem because 0 could be an int or char *,
-    // so CreateBVConst was ambiguous.
-    ASTNode CreateBVConst(const char *strval, int base);
-
-    //FIXME This is a dangerous function 
-    ASTNode CreateBVConst(CBV bv, unsigned width);
-
-    // Create and return an interior ASTNode
-    ASTNode CreateNode(Kind kind, const ASTVec &children = _empty_ASTVec);
-
-    ASTNode CreateNode(Kind kind,
-		       const ASTNode& child0,
-		       const ASTVec &children = _empty_ASTVec);
-
-    ASTNode CreateNode(Kind kind,
-		       const ASTNode& child0,
-		       const ASTNode& child1,
-		       const ASTVec &children = _empty_ASTVec);    
-
-    ASTNode CreateNode(Kind kind,
-		       const ASTNode& child0,
-		       const ASTNode& child1,
-		       const ASTNode& child2,
-		       const ASTVec &children = _empty_ASTVec);
-
-    // Create and return an ASTNode for a term
-    inline ASTNode CreateTerm(Kind kind, 
-		       unsigned int width, 
-		       const ASTVec &children = _empty_ASTVec) {
-      if(!is_Term_kind(kind))
-	FatalError("CreateTerm:  Illegal kind to CreateTerm:",ASTUndefined, kind);
-      ASTNode n = CreateNode(kind, children);
-      n.SetValueWidth(width);
-
-      //by default we assume that the term is a Bitvector. If
-      //necessary the indexwidth can be changed later
-      n.SetIndexWidth(0);
-      return n;
-    }
-
-    inline ASTNode CreateTerm(Kind kind,
-		       unsigned int width,
-		       const ASTNode& child0,
-		       const ASTVec &children = _empty_ASTVec) {
-      if(!is_Term_kind(kind))
-	FatalError("CreateTerm:  Illegal kind to CreateTerm:",ASTUndefined, kind);
-      ASTNode n = CreateNode(kind, child0, children);
-      n.SetValueWidth(width);
-      return n;
-    }
-     
-    inline ASTNode CreateTerm(Kind kind,
-		       unsigned int width,
-		       const ASTNode& child0,
-		       const ASTNode& child1,
-		       const ASTVec &children = _empty_ASTVec) {
-      if(!is_Term_kind(kind))
-	FatalError("CreateTerm:  Illegal kind to CreateTerm:",ASTUndefined, kind);
-      ASTNode n = CreateNode(kind, child0, child1, children);
-      n.SetValueWidth(width);
-      return n;
-    }
-
-    inline ASTNode CreateTerm(Kind kind,
-		       unsigned int width,
-		       const ASTNode& child0,
-		       const ASTNode& child1,
-		       const ASTNode& child2,
-		       const ASTVec &children = _empty_ASTVec) {
-      if(!is_Term_kind(kind))
-	FatalError("CreateTerm:  Illegal kind to CreateTerm:",ASTUndefined, kind);
-      ASTNode n = CreateNode(kind, child0, child1, child2, children);
-      n.SetValueWidth(width);
-      return n;
-    }
-
-    ASTNode SimplifyFormula_NoRemoveWrites(const ASTNode& a, bool pushNeg);
-    ASTNode SimplifyFormula_TopLevel(const ASTNode& a, bool pushNeg);
-    ASTNode SimplifyFormula(const ASTNode& a, bool pushNeg);
-    ASTNode SimplifyTerm_TopLevel(const ASTNode& b);
-    ASTNode SimplifyTerm(const ASTNode& a);
-    void CheckSimplifyInvariant(const ASTNode& a, const ASTNode& output);    
-  private:
-    //memo table for simplifcation
-    ASTNodeMap SimplifyMap;
-    ASTNodeMap SimplifyNegMap;
-    ASTNodeMap SolverMap;
-    ASTNodeSet AlwaysTrueFormMap;
-    ASTNodeMap MultInverseMap;
-
-  public:
-    ASTNode SimplifyAtomicFormula(const ASTNode& a, bool pushNeg);
-    ASTNode CreateSimplifiedEQ(const ASTNode& t1, const ASTNode& t2);
-    ASTNode ITEOpt_InEqs(const ASTNode& in1);
-    ASTNode CreateSimplifiedTermITE(const ASTNode& t1, const ASTNode& t2, const ASTNode& t3);
-    ASTNode CreateSimplifiedINEQ(Kind k, const ASTNode& a0, const ASTNode& a1, bool pushNeg);
-    ASTNode SimplifyNotFormula(const ASTNode& a, bool pushNeg);
-    ASTNode SimplifyAndOrFormula(const ASTNode& a, bool pushNeg);
-    ASTNode SimplifyXorFormula(const ASTNode& a, bool pushNeg);
-    ASTNode SimplifyNandFormula(const ASTNode& a, bool pushNeg);
-    ASTNode SimplifyNorFormula(const ASTNode& a, bool pushNeg);
-    ASTNode SimplifyImpliesFormula(const ASTNode& a, bool pushNeg);
-    ASTNode SimplifyIffFormula(const ASTNode& a, bool pushNeg);
-    ASTNode SimplifyIteFormula(const ASTNode& a, bool pushNeg);
-    ASTNode FlattenOneLevel(const ASTNode& a);
-    ASTNode FlattenAndOr(const ASTNode& a);
-    ASTNode CombineLikeTerms(const ASTNode& a);
-    ASTNode LhsMinusRhs(const ASTNode& eq);
-    ASTNode DistributeMultOverPlus(const ASTNode& a, 
-				   bool startdistribution=false);
-    ASTNode ConvertBVSXToITE(const ASTNode& a);
-    //checks if the input constant is odd or not
-    bool BVConstIsOdd(const ASTNode& c);
-    //computes the multiplicatve inverse of the input
-    ASTNode MultiplicativeInverse(const ASTNode& c);
- 
-    void ClearAllTables(void);
-    void ClearAllCaches(void);
-    int  BeforeSAT_ResultCheck(const ASTNode& q);
-    int  CallSAT_ResultCheck(MINISAT::Solver& newS, 
-			     const ASTNode& q, const ASTNode& orig_input);   
-    int  SATBased_ArrayReadRefinement(MINISAT::Solver& newS, 
-				      const ASTNode& q, const ASTNode& orig_input);
-    int SATBased_ArrayWriteRefinement(MINISAT::Solver& newS, const ASTNode& orig_input);
-    //creates array write axiom only for the input term or formula, if
-    //necessary. If there are no axioms to produce then it simply
-    //generates TRUE
-    ASTNode Create_ArrayWriteAxioms(const ASTNode& array_readoverwrite_term, const ASTNode& array_newname);
-    ASTVec ArrayWrite_RemainingAxioms;
-    //variable indicates that counterexample will now be checked by
-    //the counterexample checker, and hence simplifyterm must switch
-    //off certain optimizations. In particular, array write
-    //optimizations
-    bool start_abstracting;
-    bool Begin_RemoveWrites;
-    bool SimplifyWrites_InPlace_Flag;
-
-    void CopySolverMap_To_CounterExample(void);
-    //int LinearSearch(const ASTNode& orig_input);    
-    //Datastructures and functions needed for counterexample
-    //generation, and interface with MINISAT
-  private:
-    /* MAP: This is a map from ASTNodes to MINISAT::Vars. 
-     *
-     * The map is populated while ASTclauses are read from the AST
-     * ClauseList returned by CNF converter. For every new boolean
-     * variable in ASTClause a new MINISAT::Var is created (these vars
-     * typedefs for ints)
-     */
-    typedef hash_map<ASTNode, MINISAT::Var, 
-		     ASTNode::ASTNodeHasher, 
-		     ASTNode::ASTNodeEqual> ASTtoSATMap;        
-    ASTtoSATMap _ASTNode_to_SATVar;
-
-  public:  
-    //converts the clause to SAT and calls SAT solver
-    bool toSATandSolve(MINISAT::Solver& S, ClauseList& cll);
-
-    ///print SAT solver statistics
-    void PrintStats(MINISAT::SolverStats& stats);
-
-    //accepts query and returns the answer. if query is valid, return
-    //true, else return false. Automatically constructs counterexample
-    //for invalid queries, and prints them upon request.
-    int TopLevelSAT(const ASTNode& query, const ASTNode& asserts);
-
-    // Debugging function to find problems in BitBlast and ToCNF.
-    // See body in ToSAT.cpp for more explanation.
-    ASTNode CheckBBandCNF(MINISAT::Solver& newS, ASTNode form);
-
-    // Internal recursive body of above.
-    ASTNode CheckBBandCNF_int(MINISAT::Solver& newS, ASTNode form);
-
-    // Helper function for CheckBBandCNF
-    ASTNode SymbolTruthValue(MINISAT::Solver &newS, ASTNode form); 
-
-    //looksup a MINISAT var from the minisat-var memo-table. if none
-    //exists, then creates one.
-    MINISAT::Var LookupOrCreateSATVar(MINISAT::Solver& S, const ASTNode& n);
-
-    // Memo table for CheckBBandCNF debugging function
-    ASTNodeMap CheckBBandCNFMemo;
-
-
-    //Data structures for Array Read Transformations
-  private:
-    /* MAP: This is a map from Array Names to list of array-read
-     * indices in the input. This map is used by the TransformArray()
-     * function
-     *
-     * This map is useful in converting array reads into nested ITE
-     * constructs. Suppose there are two array reads in the input
-     * Read(A,i) and Read(A,j). Then Read(A,i) is replaced with a
-     * symbolic constant, say v1, and Read(A,j) is replaced with the
-     * following ITE:
-     *
-     * ITE(i=j,v1,v2)
-     */
-    //CAUTION: I tried using a set instead of vector for
-    //readindicies. for some odd reason the performance went down
-    //considerably. this is totally inexplicable.
-    ASTNodeToVecMap _arrayname_readindices;
-        
-    /* MAP: This is a map from Array Names to nested ITE constructs,
-     * which are built as described below. This map is used by the
-     * TransformArray() function
-     *
-     * This map is useful in converting array reads into nested ITE
-     * constructs. Suppose there are two array reads in the input
-     * Read(A,i) and Read(A,j). Then Read(A,i) is replaced with a
-     * symbolic constant, say v1, and Read(A,j) is replaced with the
-     * following ITE:
-     *
-     * ITE(i=j,v1,v2)
-     */
-    ASTNodeMap _arrayread_ite;
-
-    /*MAP: This is a map from array-reads to symbolic constants. This
-     *map is used by the TransformArray()
-     */
-    ASTNodeMap _arrayread_symbol;
-
-    ASTNodeSet _introduced_symbols;
-
-    /*Memoization map for TransformFormula/TransformTerm/TransformArray function
-     */
-    ASTNodeMap TransformMap;
-    
-    //count to keep track of new symbolic constants introduced
-    //corresponding to Array Reads
-    unsigned int _symbol_count;
-
-    //Formula/Term Transformers. Let Expr Manager, Type Checker
-  public:
-    //Functions that Transform ASTNodes
-    ASTNode TransformFormula(const ASTNode& query);
-    ASTNode TransformTerm(const ASTNode& term);
-    ASTNode TransformArray(const ASTNode& term);
-    ASTNode TranslateSignedDivMod(const ASTNode& term);
-
-    //LET Management
-  private:
-    // MAP: This map is from bound IDs that occur in LETs to
-    // expression. The map is useful in checking replacing the IDs
-    // with the corresponding expressions.
-    ASTNodeMap _letid_expr_map;
-  public:
-
-    ASTNode ResolveID(const ASTNode& var);
-
-    //Functions that are used to manage LET expressions
-    void LetExprMgr(const ASTNode& var, const ASTNode& letExpr);
-
-    //Delete Letid Map
-    void CleanupLetIDMap(void);
-
-    //Allocate LetID map
-    void InitializeLetIDMap(void);
-
-    //Substitute Let-vars with LetExprs
-    ASTNode SubstituteLetExpr(ASTNode inExpr);
-
-    /* MAP: This is a map from MINISAT::Vars to ASTNodes
-     *
-     * This is a reverse map, useful in constructing
-     * counterexamples. MINISAT returns a model in terms of MINISAT
-     * Vars, and this map helps us convert it to a model over ASTNode
-     * variables.
-     */    
-    vector<ASTNode> _SATVar_to_AST;
-
-  private:        
-    /* MAP: This is a map from ASTNodes to vectors of bits
-     *
-     * This map is used in constructing and printing
-     * counterexamples. MINISAT returns values for each bit (a
-     * BVGETBIT Node), and this maps allows us to assemble the bits
-     * into bitvectors.
-     */    
-    typedef hash_map<ASTNode, hash_map<unsigned int, bool> *, 
-		     ASTNode::ASTNodeHasher, 
-		     ASTNode::ASTNodeEqual> ASTtoBitvectorMap;        
-    ASTtoBitvectorMap _ASTNode_to_Bitvector;
-
-    //Data structure that holds the counter-model
-    ASTNodeMap CounterExampleMap;
-
-    //Checks if the counter_example is ok. In order for the
-    //counter_example to be ok, Every assert must evaluate to true 
-    //w.r.t couner_example and the query must evaluate to
-    //false. Otherwise the counter_example is bogus.
-    void CheckCounterExample(bool t);    
-
-    //Converts a vector of bools to a BVConst
-    ASTNode BoolVectoBVConst(hash_map<unsigned,bool> * w, unsigned int l);
-
-    //accepts a term and turns it into a constant-term w.r.t counter_example 
-    ASTNode TermToConstTermUsingModel(const ASTNode& term, bool ArrayReadFlag = true);
-    ASTNode Expand_ReadOverWrite_UsingModel(const ASTNode& term, bool ArrayReadFlag = true);
-    //Computes the truth value of a formula w.r.t counter_example
-    ASTNode ComputeFormulaUsingModel(const ASTNode& form);
-
-    //Replaces WRITE(Arr,i,val) with ITE(j=i, val, READ(Arr,j))
-    ASTNode RemoveWrites_TopLevel(const ASTNode& term);
-    ASTNode RemoveWrites(const ASTNode& term);
-    ASTNode SimplifyWrites_InPlace(const ASTNode& term);
-    ASTNode ReadOverWrite_To_ITE(const ASTNode& term);
-
-    ASTNode NewArrayVar(unsigned int index, unsigned int value);
-    ASTNode NewVar(unsigned int valuewidth);
-    //For ArrayWrite Abstraction: map from read-over-write term to
-    //newname.
-    ASTNodeMap ReadOverWrite_NewName_Map;
-    //For ArrayWrite Refinement: Map new arraynames to Read-Over-Write
-    //terms
-    ASTNodeMap NewName_ReadOverWrite_Map;
-    
-  public:
-    //print the STP solver output
-    void PrintOutput(bool true_iff_valid);
-
-    //Converts MINISAT counterexample into an AST memotable (i.e. the
-    //function populates the datastructure CounterExampleMap)
-    void ConstructCounterExample(MINISAT::Solver& S);
-
-    //Prints the counterexample to stdout
-    void PrintCounterExample(bool t,std::ostream& os=cout);
-
-    //Prints the counterexample to stdout
-    void PrintCounterExample_InOrder(bool t);
-
-    //queries the counterexample, and returns the value corresponding
-    //to e
-    ASTNode GetCounterExample(bool t, const ASTNode& e);
-
-    int CounterExampleSize(void) const {return CounterExampleMap.size();}
-
-    //FIXME: This is bloody dangerous function. Hack attack to take
-    //care of requests from users who want to store complete
-    //counter-examples in their own data structures.
-    ASTNodeMap GetCompleteCounterExample() {return CounterExampleMap;}
-
-    // prints MINISAT assigment one bit at a time, for debugging.
-    void PrintSATModel(MINISAT::Solver& S);
-
-    //accepts constant input and normalizes it. 
-    ASTNode BVConstEvaluator(const ASTNode& t);
-
-    //FUNCTION TypeChecker: Assumes that the immediate Children of the
-    //input ASTNode have been typechecked. This function is suitable
-    //in scenarios like where you are building the ASTNode Tree, and
-    //you typecheck as you go along. It is not suitable as a general
-    //typechecker
-    void BVTypeCheck(const ASTNode& n);
-    
-  private:
-    //stack of Logical Context. each entry in the stack is a logical
-    //context. A logical context is a vector of assertions. The
-    //logical context is represented by a ptr to a vector of
-    //assertions in that logical context. Logical contexts are created
-    //by PUSH/POP
-    std::vector<ASTVec *>  _asserts;
-    //The query for the current logical context.
-    ASTNode _current_query;
-
-    //this flag, when true, indicates that counterexample is being
-    //checked by the counterexample checker
-    bool counterexample_checking_during_refinement;
-
-    //this flag indicates as to whether the input has been determined to
-    //be valid or not by this tool
-    bool ValidFlag;
-
-    //this flag, when true, indicates that a BVDIV divide by zero
-    //exception occured. However, the program must not exit with a
-    //fatalerror. Instead, it should evaluate the whole formula (which
-    //contains the BVDIV term) to be FALSE.
-    bool bvdiv_exception_occured;
-
-  public:
-    //set of functions that manipulate Logical Contexts.
-    //
-    //add an assertion to the current logical context
-    void AddAssert(const ASTNode& assert);
-    void Push(void);
-    void Pop(void);
-    void AddQuery(const ASTNode& q);    
-    const ASTNode PopQuery();
-    const ASTNode GetQuery();
-    const ASTVec GetAsserts(void);
-
-    //reports node size.  Second arg is "clearstatinfo", whatever that is.
-    unsigned int NodeSize(const ASTNode& a, bool t = false);
-
-  private:
-    //This memo map is used by the ComputeFormulaUsingModel()
-    ASTNodeMap ComputeFormulaMap;
-    //Map for statiscal purposes
-    ASTNodeSet StatInfoSet;
-
-
-    ASTNodeMap TermsAlreadySeenMap;
-    ASTNode CreateSubstitutionMap(const ASTNode& a);
-  public:
-    //prints statistics for the ASTNode. can add a prefix string c
-    void ASTNodeStats(const char * c, const ASTNode& a);
-
-    //substitution
-    bool CheckSubstitutionMap(const ASTNode& a, ASTNode& output);  
-    bool CheckSubstitutionMap(const ASTNode& a);
-    bool UpdateSubstitutionMap(const ASTNode& e0, const ASTNode& e1);
-    //if (a > b) in the termorder, then return 1
-    //elseif (a < b) in the termorder, then return -1
-    //else return 0
-    int TermOrder(const ASTNode& a, const ASTNode& b);
-    //fill the arrayname_readindices vector if e0 is a READ(Arr,index)
-    //and index is a BVCONST
-    void FillUp_ArrReadIndex_Vec(const ASTNode& e0, const ASTNode& e1);
-    bool VarSeenInTerm(const ASTNode& var, const ASTNode& term);
-
-    //functions for checking and updating simplifcation map
-    bool CheckSimplifyMap(const ASTNode& key, ASTNode& output, bool pushNeg);
-    void UpdateSimplifyMap(const ASTNode& key, const ASTNode& value, bool pushNeg);
-    bool CheckAlwaysTrueFormMap(const ASTNode& key);
-    void UpdateAlwaysTrueFormMap(const ASTNode& val);
-    bool CheckMultInverseMap(const ASTNode& key, ASTNode& output);
-    void UpdateMultInverseMap(const ASTNode& key, const ASTNode& value);
-
-    //Map for solved variables
-    bool CheckSolverMap(const ASTNode& a, ASTNode& output);
-    bool CheckSolverMap(const ASTNode& a);
-    bool UpdateSolverMap(const ASTNode& e0, const ASTNode& e1);
-  public:
-    //FIXME: HACK_ATTACK. this vector was hacked into the code to
-    //support a special request by Dawson' group. They want the
-    //counterexample to be printed in the order of variables declared.
-    //TO BE COMMENTED LATER (say by 1st week of march,2006)
-    ASTVec _special_print_set;
-
-    //prints the initial activity levels of variables
-    void PrintActivityLevels_Of_SATVars(char * init_msg, MINISAT::Solver& newS);
-
-    //this function biases the activity levels of MINISAT variables.
-    void ChangeActivityLevels_Of_SATVars(MINISAT::Solver& n);
-
-    // Constructor
-    BeevMgr() : _interior_unique_table(INITIAL_INTERIOR_UNIQUE_TABLE_SIZE),
-		_symbol_unique_table(INITIAL_SYMBOL_UNIQUE_TABLE_SIZE),
-		_bvconst_unique_table(INITIAL_BVCONST_UNIQUE_TABLE_SIZE),
-		BBTermMemo(INITIAL_BBTERM_MEMO_TABLE_SIZE),
-		BBFormMemo(INITIAL_BBFORM_MEMO_TABLE_SIZE),
-		_max_node_num(0),
-		ASTFalse(CreateNode(FALSE)),
-		ASTTrue(CreateNode(TRUE)),
-		ASTUndefined(CreateNode(UNDEFINED)),
-		SimplifyMap(INITIAL_SIMPLIFY_MAP_SIZE),
-		SimplifyNegMap(INITIAL_SIMPLIFY_MAP_SIZE),
-		SolverMap(INITIAL_SOLVER_MAP_SIZE),
-		_arrayread_symbol(INITIAL_ARRAYREAD_SYMBOL_SIZE),
-		_introduced_symbols(INITIAL_INTRODUCED_SYMBOLS_SIZE),
-		_symbol_count(0) { 
-      _current_query = ASTUndefined;
-      ValidFlag = false;
-      bvdiv_exception_occured = false;
-      counterexample_checking_during_refinement = false;
-      start_abstracting = false;
-      Begin_RemoveWrites = false;
-      SimplifyWrites_InPlace_Flag = false;
-    };
-    
-    //destructor
-    ~BeevMgr();
-  }; //End of Class BeevMgr
-
-
-  class CompleteCounterExample {
-    ASTNodeMap counterexample;
-    BeevMgr * bv;
-  public:
-    CompleteCounterExample(ASTNodeMap a, BeevMgr* beev) : counterexample(a), bv(beev){} 
-    ASTNode GetCounterExample(ASTNode e) {
-      if(BOOLEAN_TYPE == e.GetType() && SYMBOL != e.GetKind()) {
-	FatalError("You must input a term or propositional variables\n",e);
-      }
-      if(counterexample.find(e) != counterexample.end()) {
-	return counterexample[e];
-      }
-      else {
-	if(SYMBOL == e.GetKind() && BOOLEAN_TYPE == e.GetType()) {
-	  return bv->CreateNode(BEEV::FALSE);
-	}
-
-	if(SYMBOL == e.GetKind()) {
-	  ASTNode z = bv->CreateZeroConst(e.GetValueWidth());
-	  return z;
-	}
-
-	return e;	  
-      }
-    }
-  };
-
-} // end namespace BEEV
-#endif
diff --git a/stp/AST/ASTKind.cpp b/stp/AST/ASTKind.cpp
deleted file mode 100644
index 9a2392c9..00000000
--- a/stp/AST/ASTKind.cpp
+++ /dev/null
@@ -1,118 +0,0 @@
-// Generated automatically by genkinds.h from ASTKind.kinds Sun Apr  4 19:39:09 2010.
-// Do not edit
-namespace BEEV {
-const char * _kind_names[] =  {
-   "UNDEFINED",
-   "SYMBOL",
-   "BVCONST",
-   "BVNEG",
-   "BVCONCAT",
-   "BVOR",
-   "BVAND",
-   "BVXOR",
-   "BVNAND",
-   "BVNOR",
-   "BVXNOR",
-   "BVEXTRACT",
-   "BVLEFTSHIFT",
-   "BVRIGHTSHIFT",
-   "BVSRSHIFT",
-   "BVVARSHIFT",
-   "BVPLUS",
-   "BVSUB",
-   "BVUMINUS",
-   "BVMULTINVERSE",
-   "BVMULT",
-   "BVDIV",
-   "BVMOD",
-   "SBVDIV",
-   "SBVMOD",
-   "BVSX",
-   "BOOLVEC",
-   "ITE",
-   "BVGETBIT",
-   "BVLT",
-   "BVLE",
-   "BVGT",
-   "BVGE",
-   "BVSLT",
-   "BVSLE",
-   "BVSGT",
-   "BVSGE",
-   "EQ",
-   "NEQ",
-   "FALSE",
-   "TRUE",
-   "NOT",
-   "AND",
-   "OR",
-   "NAND",
-   "NOR",
-   "XOR",
-   "IFF",
-   "IMPLIES",
-   "READ",
-   "WRITE",
-   "ARRAY",
-   "BITVECTOR",
-   "BOOLEAN",
-};
-
-unsigned char _kind_categories[] = {
-   0,
-   3,
-   1,
-   1,
-   1,
-   1,
-   1,
-   1,
-   1,
-   1,
-   1,
-   1,
-   1,
-   1,
-   1,
-   1,
-   1,
-   1,
-   1,
-   1,
-   1,
-   1,
-   1,
-   1,
-   1,
-   1,
-   1,
-   3,
-   2,
-   2,
-   2,
-   2,
-   2,
-   2,
-   2,
-   2,
-   2,
-   2,
-   2,
-   2,
-   2,
-   2,
-   2,
-   2,
-   2,
-   2,
-   2,
-   2,
-   2,
-   1,
-   1,
-   0,
-   0,
-   0,
-};
-
-}  // end namespace
diff --git a/stp/AST/ASTKind.h b/stp/AST/ASTKind.h
deleted file mode 100644
index 2480b6e6..00000000
--- a/stp/AST/ASTKind.h
+++ /dev/null
@@ -1,79 +0,0 @@
-// -*- c++ -*-
-#ifndef TESTKINDS_H
-#define TESTKINDS_H
-// Generated automatically by genkinds.pl from ASTKind.kinds Sun Apr  4 19:39:09 2010.
-// Do not edit
-namespace BEEV {
-  typedef enum {
-    UNDEFINED,
-    SYMBOL,
-    BVCONST,
-    BVNEG,
-    BVCONCAT,
-    BVOR,
-    BVAND,
-    BVXOR,
-    BVNAND,
-    BVNOR,
-    BVXNOR,
-    BVEXTRACT,
-    BVLEFTSHIFT,
-    BVRIGHTSHIFT,
-    BVSRSHIFT,
-    BVVARSHIFT,
-    BVPLUS,
-    BVSUB,
-    BVUMINUS,
-    BVMULTINVERSE,
-    BVMULT,
-    BVDIV,
-    BVMOD,
-    SBVDIV,
-    SBVMOD,
-    BVSX,
-    BOOLVEC,
-    ITE,
-    BVGETBIT,
-    BVLT,
-    BVLE,
-    BVGT,
-    BVGE,
-    BVSLT,
-    BVSLE,
-    BVSGT,
-    BVSGE,
-    EQ,
-    NEQ,
-    FALSE,
-    TRUE,
-    NOT,
-    AND,
-    OR,
-    NAND,
-    NOR,
-    XOR,
-    IFF,
-    IMPLIES,
-    READ,
-    WRITE,
-    ARRAY,
-    BITVECTOR,
-    BOOLEAN
-} Kind;
-
-extern unsigned char _kind_categories[];
-
-inline bool is_Term_kind(Kind k) { return (_kind_categories[k] & 1); }
-
-inline bool is_Form_kind(Kind k) { return (_kind_categories[k] & 2); }
-
-extern const char *_kind_names[];
-
-/** Prints symbolic name of kind */
-inline ostream& operator<<(ostream &os, const Kind &kind) { os << _kind_names[kind]; return os; }
-
-
-}  // end namespace
-
-
-#endif
diff --git a/stp/AST/ASTKind.kinds b/stp/AST/ASTKind.kinds
deleted file mode 100644
index 03112eb8..00000000
--- a/stp/AST/ASTKind.kinds
+++ /dev/null
@@ -1,71 +0,0 @@
-#Please refer LICENSE FILE in the home directory for licensing information
-# name minkids maxkids cat1 cat2 ...
-Categories:	Term	Form
-
-# Leaf nodes.
-UNDEFINED	0	0
-SYMBOL		0	0	Term	Form 
-
-# These always produce terms
-BVCONST		0	0	Term
-BVNEG		1	1	Term
-BVCONCAT	2	-	Term
-BVOR		1	-	Term
-BVAND		1	-	Term
-BVXOR		1	-	Term
-BVNAND		1	-	Term
-BVNOR		1	-	Term
-BVXNOR		1	-	Term
-BVEXTRACT	3	3	Term
-BVLEFTSHIFT	3	3	Term
-BVRIGHTSHIFT	3	3	Term
-BVSRSHIFT	3	3	Term
-BVVARSHIFT	3	3	Term
-BVPLUS		1	-	Term
-BVSUB		2	2	Term
-BVUMINUS	1	1	Term
-BVMULTINVERSE	1	1	Term
-BVMULT		1	-	Term
-BVDIV		2	2	Term
-BVMOD		2	2	Term
-SBVDIV		2	2	Term
-SBVMOD		2	2	Term
-BVSX		1	1	Term
-BOOLVEC         0       -       Term
-
-# Formula OR term, depending on context
-ITE		3	3	Term	Form
-
-# These produce formulas.
-BVGETBIT	2	2	Form
-BVLT		2	2	Form
-BVLE		2	2	Form
-BVGT		2	2	Form
-BVGE		2	2	Form
-BVSLT		2	2	Form
-BVSLE		2	2	Form
-BVSGT		2	2	Form
-BVSGE		2	2	Form
-EQ		2	2	Form
-NEQ		2	2	Form
-FALSE		0	0	Form
-TRUE		0	0	Form
-NOT		1	1	Form
-AND		1	-	Form
-OR		1	-	Form
-NAND		1	-	Form
-NOR		1	-	Form
-XOR		1	-	Form
-IFF		1	-	Form
-IMPLIES		2	2	Form
-
-# array operations
-READ		2	2	Term
-WRITE		3	3	Term
-
-#Types: These kinds are used only in the API. Once processed inside
-#the API, they are never used again in the system 
-ARRAY           0       0
-BITVECTOR       0       0
-BOOLEAN         0       0
-
diff --git a/stp/AST/ASTUtil.cpp b/stp/AST/ASTUtil.cpp
deleted file mode 100644
index ecb54a4a..00000000
--- a/stp/AST/ASTUtil.cpp
+++ /dev/null
@@ -1,45 +0,0 @@
-/********************************************************************
- * AUTHORS: Vijay Ganesh, David L. Dill
- *
- * BEGIN DATE: November, 2005
- *
- * LICENSE: Please view LICENSE file in the home dir of this Program
- ********************************************************************/
-// -*- c++ -*-
-
-#include "ASTUtil.h"
-#include <ostream>
-
-namespace BEEV {
-  ostream &operator<<(ostream &os, const Spacer &sp) {
-    // Instead of wrapping lines with hundreds of spaces, prints
-    // a "+" at the beginning of the line for each wrap-around.
-    // so lines print like: +14+		(XOR ...
-    int blanks = sp._spaces % 60;
-    int wraps = sp._spaces / 60;
-    if (wraps > 0) {
-      os << "+" << wraps;
-    }
-    for (int i = 0; i < blanks; i++)
-      os << " ";  
-    return os;
-  }
-   
-  //this function accepts the name of a function (as a char *), and
-  //records some stats about it. if the input is "print_func_stats",
-  //the function will then print the stats that it has collected.
-  void CountersAndStats(const char * functionname) {
-    if(!stats)
-      return;
-    static function_counters s;
-    
-    if(!strcmp(functionname,"print_func_stats")) {
-      cout << endl;
-      for(hash_map<const char*,int,hash<const char*>,eqstr>::iterator it=s.begin(),itend=s.end();
-	  it!=itend;it++)
-	cout << "Number of times the function: " << it->first << ": is called: " << it->second << endl;
-      return;
-    }
-    s[functionname] += 1;
-  }
-} // end of namespace
diff --git a/stp/AST/ASTUtil.h b/stp/AST/ASTUtil.h
deleted file mode 100644
index c90ee0ce..00000000
--- a/stp/AST/ASTUtil.h
+++ /dev/null
@@ -1,107 +0,0 @@
-/********************************************************************
- * AUTHORS: Vijay Ganesh, David L. Dill
- *
- * BEGIN DATE: November, 2005
- *
- * LICENSE: Please view LICENSE file in the home dir of this Program
- ********************************************************************/
-// -*- c++ -*-
-
-#ifndef ASTUTIL_H
-#define ASTUTIL_H
-
-#include <cstring>
-#include <iostream>
-#include <vector>
-#ifdef EXT_HASH_MAP
-#include <ext/hash_set>
-#include <ext/hash_map>
-#else
-#include <hash_set>
-#include <hash_map>
-#endif
-
-using namespace std; 
-namespace BEEV {
-#ifdef EXT_HASH_MAP
-  using namespace __gnu_cxx;
-#endif
-  //some global variables that are set through commandline options. it
-  //is best that these variables remain global. Default values set
-  //here
-  //
-  //collect statistics on certain functions
-  extern bool stats;
-  //print DAG nodes
-  extern bool print_nodes;
-  //tentative global var to allow for variable activity optimization
-  //in the SAT solver. deprecated.
-  extern bool variable_activity_optimize;
-  //run STP in optimized mode
-  extern bool optimize;
-  //do sat refinement, i.e. underconstraint the problem, and feed to
-  //SAT. if this works, great. else, add a set of suitable constraints
-  //to re-constraint the problem correctly, and call SAT again, until
-  //all constraints have been added.
-  extern bool arrayread_refinement;
-  //switch to control write refinements
-  extern bool arraywrite_refinement;
-  //check the counterexample against the original input to STP
-  extern bool check_counterexample;
-  //construct the counterexample in terms of original variable based
-  //on the counterexample returned by SAT solver
-  extern bool construct_counterexample;
-  extern bool print_counterexample;
-  //if this option is true then print the way dawson wants using a
-  //different printer. do not use this printer.
-  extern bool print_arrayval_declaredorder;
-  //flag to decide whether to print "valid/invalid" or not
-  extern bool print_output;
-  //do linear search in the array values of an input array. experimental
-  extern bool linear_search;
-  //print the variable order chosen by the sat solver while it is
-  //solving.
-  extern bool print_sat_varorder; 
-  //turn on word level bitvector solver
-  extern bool wordlevel_solve;
-  //XOR flattening optimizations.
-  extern bool xor_flatten;
-  //this flag indicates that the BVSolver() succeeded
-  extern bool toplevel_solved;
-  //the smtlib parser has been turned on
-  extern bool smtlib_parser_enable;
-  //print the input back
-  extern bool print_STPinput_back;
-
-  extern void (*vc_error_hdlr)(const char* err_msg);
-  /*Spacer class is basically just an int, but the new class allows
-    overloading of << with a special definition that prints the int as
-    that many spaces. */
-  class Spacer {
-  public:
-    int _spaces;
-    Spacer(int spaces) { _spaces = spaces; }
-    friend ostream& operator<<(ostream& os, const Spacer &ind);
-  };
-
-  inline Spacer spaces(int width) {
-    Spacer sp(width);
-    return sp;
-  }
-
-  struct eqstr {
-    bool operator()(const char* s1, const char* s2) const {
-      return strcmp(s1, s2) == 0;
-    }
-  };
-  
-  typedef hash_map<const char*,int, 
-		   hash<const char *>,eqstr> function_counters;
-  void CountersAndStats(const char * functionname);
-
-  //global function which accepts an integer and looks up the
-  //corresponding ASTNode and prints a char* of that ASTNode
-  void Convert_MINISATVar_To_ASTNode_Print(int minisat_var, 
-					   int decision, int polarity=0);
-} // end namespace.
-#endif
diff --git a/stp/AST/BitBlast.cpp b/stp/AST/BitBlast.cpp
deleted file mode 100644
index de78ec74..00000000
--- a/stp/AST/BitBlast.cpp
+++ /dev/null
@@ -1,812 +0,0 @@
-/********************************************************************
- * AUTHORS: David L. Dill, Vijay Ganesh
- *
- * BEGIN DATE: November, 2005
- *
- * LICENSE: Please view LICENSE file in the home dir of this Program
- ********************************************************************/
-// -*- c++ -*-
-
-// BitBlast -- convert bitvector terms and formulas to boolean
-// formulas.  A term is something that can represent a multi-bit
-// bitvector, such as BVPLUS or BVXOR (or a BV variable or constant).
-// A formula (form) represents a boolean value, such as EQ or BVLE.
-// Bit blasting a term representing an n-bit bitvector with BBTerm
-// yields a vector of n boolean formulas (returning ASTVec).
-// Bit blasting a formula returns a single boolean formula (type ASTNode).
-
-// A bitblasted term is a vector of ASTNodes for formulas.
-// The 0th element of the vector corresponds to bit 0 -- the low-order bit.
-
-#include "AST.h"
-namespace BEEV {
-  //  extern void lpvec(ASTVec &vec);
-
-// FIXME: Assert no zero-length bit vectors!!!
-// FIXME: Need top-level functions that create and destroy the memo tables.
-// FIXME:  Check resource limits and generate an exception when exceeded.
-// FIXME:  THis does a lot of unnecessary copying of vectors.
-//    Had to be careful not to modify memoized vectors!
-// FIXME:  Might be some redundant variables.
-
-// accepts a term, and returns a vector of bitblasted bits(ASTVec)
-
-ASTNode ASTJunk;
-const ASTNode BeevMgr::BBTerm(const ASTNode& term) {
-  //CHANGED TermMemo is now an ASTNodeMap. Based on BBFormMemo
-  ASTNodeMap::iterator it = BBTermMemo.find(term);
-  if (it != BBTermMemo.end()) {
-    // already there.  Just return it.
-    return it->second;
-  }
-
-//  ASTNode& result = ASTJunk;
-  ASTNode result;
-
-  Kind k = term.GetKind();
-  if (!is_Term_kind(k))
-    FatalError("BBTerm: Illegal kind to BBTerm",term);
-
-  ASTVec::const_iterator kids_end = term.end(); 
-  unsigned int num_bits = term.GetValueWidth();
-  switch (k) {
-  case BVNEG: {
-    // bitwise complement
-    // bitblast the child.
-    //FIXME Uses a tempory const ASTNode
-    const ASTNode& bbkids = BBTerm(term[0]);
-    result = CreateNode(BOOLVEC, BBNeg(bbkids.GetChildren()));
-    break;
-  }
-  case BVSRSHIFT:
-  case BVVARSHIFT: 
-    FatalError("BBTerm: These kinds have not been implemented in the BitBlaster: ", term);
-    break;
-  case ITE: {
-    // Term version of ITE.
-
-    // Blast the args
-    // FIXME Uses temporary const ASTNodes and an ASTVec&
-    const ASTNode& cond = BBForm(term[0]);
-    const ASTNode& thn = BBTerm(term[1]);
-    const ASTNode& els = BBTerm(term[2]);
-    result = 
-       CreateNode(BOOLVEC, BBITE(cond, thn.GetChildren(), els.GetChildren()));
-    break;
-  }
-  case BVSX: {
-    // Replicate high-order bit as many times as necessary.
-    // Arg 0 is expression to be sign extended.
-    const ASTNode& arg = term[0];
-    unsigned long result_width = term.GetValueWidth();
-    unsigned long arg_width = arg.GetValueWidth();
-    //FIXME Uses a temporary const ASTNode reference
-    const ASTNode& bbarg = BBTerm(arg);
-
-    if (result_width == arg_width) {
-      //nothing to sign extend
-      break;
-    }
-    else {
-      //we need to sign extend
-      const ASTNode& msbX = bbarg.back();
-      //const ASTNode& msb1 = msbX;
-      
-      ASTVec ccc = msbX.GetChildren();
-      const ASTNode& msb = CreateSimpForm(msbX.GetKind(),ccc);
-
-     //  Old version
-     //  ASTNode msb = bbarg.back();
-     //  const ASTNode msb1 = msb;
-      
-     //  ASTVec ccc = msb.GetChildren();
-     //  msb = CreateSimpForm(msb.GetKind(),ccc);
-
-      // DD 1/14/07 Simplify silently drops all but first two args of XOR.
-      // I expanded XOR to N args with flattening optimization.
-      // This bug took 2 days to track down!
-
-      // msb = SimplifyFormula(msb,false);
-
-      // cout << "!!!!!!!!!!!!!!!!" << endl
-      // << "Simplify msb:" << msb2 << endl
-      // << "Simplify result:" << msb << endl;
-
-      //FIXME Dynamically allocate the result vector?
-      //Is this doing multiple copies?
-      //ASTVec& tmp_res = *(new ASTVec(result_width));
-      ASTVec tmp_res(result_width);
-
-      //FIXME Should these be gotten from result?
-      ASTVec::const_iterator bb_it = bbarg.begin();
-      ASTVec::iterator res_it = tmp_res.begin();
-      ASTVec::iterator res_ext = res_it+arg_width; // first bit of extended part
-      ASTVec::iterator res_end = tmp_res.end();
-      // copy LSBs directly from bbvec
-      for( ; res_it < res_ext; (res_it++, bb_it++)) {
-	*res_it = *bb_it;
-      }
-      // repeat MSB to fill up rest of result.
-      for( ; res_it < res_end; (res_it++, bb_it++)) {
-	*res_it = msb;
-      }
-      
-       //Temporary debugging code
-       //    cout << "Sign extending:" << endl 
-       //	        << "  Vec ";
-       //    lpvec( bbarg.GetChildren() );
-       //    cout << "  Extended to ";
-       //    lp(result);
-       //    cout << endl;
-      
-      result = CreateNode(BOOLVEC, tmp_res);
-
-      break;
-    }
-  }
-  case BVEXTRACT: {
-    // bitblast the child, then extract the relevant bits.
-    // Note: This could be optimized by not bitblasting the bits
-    // that aren't fetched.  But that would be tricky, especially
-    // with memo-ization.
-
-    //FIXME Using const ASTNode w/out reference
-    const ASTNode& bbkids = BBTerm(term[0]); 
-    unsigned int high = GetUnsignedConst(term[1]);
-    unsigned int low = GetUnsignedConst(term[2]);
-
-    ASTVec::const_iterator bbkfit = bbkids.begin();
-    // I should have used pointers to ASTVec, to avoid this crock
-    
-    //FIXME Creates a new local ASTVec and does the CreateNode from that
-    result = CreateNode(BOOLVEC, ASTVec(bbkfit+low, bbkfit+high+1));
-    break;
-  }
-  case BVCONCAT: {
-    //FIXME Using temporary const ASTNodes 
-    const ASTNode& vec1 = BBTerm(term[0]);
-    const ASTNode& vec2 = BBTerm(term[1]);
-
-    //FIXME This has to be an unnessecary copy and a memory leak
-    //Leaking ASTVec tmp_res = *(new ASTVec(vec2.GetChildren()));
-    ASTVec tmp_res(vec2.GetChildren());
-    tmp_res.insert(tmp_res.end(), vec1.begin(), vec1.end());
-    result = CreateNode(BOOLVEC, tmp_res);
-    break;
-  }
-  case BVPLUS: {
-    // ASSERT: at least one child.
-    // ASSERT: all children and result are the same size.
-    // Previous phase must make sure this is true.
-    // Add children pairwise and accumulate in BBsum
-
-    // FIXME: Unnecessary array copies.
-    ASTVec::const_iterator it = term.begin();
-    ASTVec tmp_res = BBTerm(*it).GetChildren();
-    for (++it; it < kids_end; it++) {
-      const ASTVec& tmp = BBTerm(*it).GetChildren();
-      BBPlus2(tmp_res, tmp, ASTFalse);
-    }
-
-    result = CreateNode(BOOLVEC, tmp_res);
-    break;
-  }
-  case BVUMINUS: {
-    //FIXME Using const ASTNode reference
-    const ASTNode& bbkid = BBTerm(term[0]);
-    result = CreateNode(BOOLVEC, BBUminus(bbkid.GetChildren()));
-    break;
-  }
-  case BVSUB: {
-    // complement of subtrahend
-    // copy, since BBSub writes into it.
-    
-    //FIXME: Unnecessary array copies?
-    ASTVec tmp_res = BBTerm(term[0]).GetChildren(); 
-
-    const ASTVec& bbkid1 = BBTerm(term[1]).GetChildren();
-    BBSub(tmp_res, bbkid1);
-    result = CreateNode(BOOLVEC, tmp_res);
-    break;
-  }
-  case BVMULT: {
-    // ASSERT 2 arguments, same length, result is same length.
-
-    const ASTNode& t0 = term[0];
-    const ASTNode& t1 = term[1];
-
-    const ASTNode& mpcd1 = BBTerm(t0);
-    const ASTNode& mpcd2 = BBTerm(t1);
-    //Reverese the order of the nodes w/out the need for temporaries
-    //This is needed because t0 an t1 must be const
-    if ((BVCONST != t0.GetKind()) && (BVCONST == t1.GetKind())) {
-      result = CreateNode(BOOLVEC, 
-        BBMult(mpcd2.GetChildren(), mpcd1.GetChildren()) );
-    }else{
-      result = CreateNode(BOOLVEC, 
-        BBMult(mpcd1.GetChildren(), mpcd2.GetChildren()) );
-    }
-    break;
-  }
-  case BVDIV:
-  case BVMOD: {
-    const ASTNode& dvdd = BBTerm(term[0]);
-    const ASTNode& dvsr = BBTerm(term[1]);
-    unsigned int width = dvdd.Degree();
-    ASTVec q(width); 
-    ASTVec r(width); 
-    BBDivMod(dvdd.GetChildren(),  dvsr.GetChildren(), q, r, width);
-    if (k == BVDIV)
-      result = CreateNode(BOOLVEC, q);    
-    else
-      result = CreateNode(BOOLVEC, r);
-    break;
-  }
-  //  n-ary bitwise operators.
-  case BVXOR:
-  case BVXNOR:
-  case BVAND:
-  case BVOR:
-  case BVNOR:
-  case BVNAND: {
-    // Add children pairwise and accumulate in BBsum
-    ASTVec::const_iterator it = term.begin();
-    Kind bk = UNDEFINED;  // Kind of individual bit op.
-    switch (k) {
-    case BVXOR: bk = XOR;  break;
-    case BVXNOR: bk = IFF; break;
-    case BVAND: bk = AND; break;
-    case BVOR: bk = OR; break;
-    case BVNOR: bk = NOR; break;
-    case BVNAND: bk = NAND; break;
-    default:
-      FatalError("BBTerm: Illegal kind to BBTerm",term);
-      break;
-    }
-
-    // Sum is destructively modified in the loop, so make a copy of value
-    // returned by BBTerm.
-    ASTNode temp = BBTerm(*it);
-    ASTVec sum(temp.GetChildren());	// First operand.
-
-    // Iterate over remaining bitvector term operands
-    for (++it; it < kids_end; it++) {
-      //FIXME FIXME FIXME: Why does using a temp. var change the behavior?
-      temp = BBTerm(*it);
-      const ASTVec& y = temp.GetChildren();
-      
-      // Iterate over bits
-      // FIXME: Why is this not using an iterator???
-      int n = y.size();
-      for (int i = 0; i < n; i++) {
-	sum[i] = CreateSimpForm(bk, sum[i], y[i]);
-      }
-    }
-    result = CreateNode(BOOLVEC, sum);
-    break;
-  }
-  case SYMBOL: {
-    // ASSERT: IndexWidth = 0?  Semantic analysis should check.
-    //Leaking ASTVec& bbvec = *(new ASTVec);
-    
-    //FIXME Why is isn't this ASTVEC bbvec(num_bits) ?
-    ASTVec bbvec;
-    for (unsigned int i = 0; i < num_bits; i++) {
-      ASTNode bit_node =
-	CreateNode(BVGETBIT, term, CreateBVConst(32,i));
-      bbvec.push_back(bit_node); 
-    }
-    result = CreateNode(BOOLVEC, bbvec);
-    break;
-  }
-  case BVCONST: {
-    ASTVec tmp_res(num_bits);
-#ifndef NATIVE_C_ARITH
-    CBV bv = term.GetBVConst();
-    for(unsigned int i = 0; i < num_bits; i++){
-      tmp_res[i] = CONSTANTBV::BitVector_bit_test(bv,i) ? ASTTrue : ASTFalse; 
-    }  
-#else
-    const unsigned long long int c = term.GetBVConst();
-    unsigned long long int bitmask = 0x00000000000000001LL;
-    for (unsigned int i = 0; i < num_bits; i++, bitmask <<= 1)
-      tmp_res[i] = ((c & (bitmask)) ? ASTTrue : ASTFalse);    
-#endif
-    result = CreateNode(BOOLVEC, tmp_res);
-    break;
-  }		  
-  case BOOLVEC: {
-    cerr << "Hit a boolvec! what to do?" << endl;
-    break;
-  }
-  default:
-    FatalError("BBTerm: Illegal kind to BBTerm",term);
-  }
-
-  //if(result == ASTJunk)
-  //  cout<<"result does not change"<<endl;
-  // cout << "================" << endl << "BBTerm:" << term << endl;
-  // cout << "----------------" << endl << "BBTerm result:";
-  // lpvec(result);
-  // cout << endl;
-
-  return (BBTermMemo[term] = result);
-
-}
-
-// bit blast a formula (boolean term).  Result is one bit wide,
-// so it returns a single ASTNode.
-// FIXME:  Add IsNegated flag.
-const ASTNode BeevMgr::BBForm(const ASTNode& form)
-{
-
-  ASTNodeMap::iterator it = BBFormMemo.find(form);
-  if (it != BBFormMemo.end()) {
-    // already there.  Just return it.
-    return it->second;
-  }
-
-  ASTNode result = ASTUndefined;
-
-  Kind k = form.GetKind();
-  if (!is_Form_kind(k)) {
-    FatalError("BBForm: Illegal kind: ",form);
-  }
-
-  //  Not returning until end, and memoizing everything, makes it easier
-  // to trace coherently.
-    
-  // Various special cases
-  switch (k) {
-  case TRUE:
-  case FALSE: {
-    result = form;
-    break;
-  }
-
-  case SYMBOL:
-    if (form.GetType() != BOOLEAN_TYPE) {
-      FatalError("BBForm: Symbol represents more than one bit", form);
-    }
-
-    result = form;
-    break;
-
-  case BVGETBIT: {
-    // exactly two children
-    const ASTNode bbchild = BBTerm(form[0]);
-    unsigned int index =  GetUnsignedConst(form[1]);
-    result = bbchild[index];
-    break;
-  }
-
-  case NOT:
-    result = CreateSimpNot(BBForm(form[0]));
-    break;  
-
-  case ITE:
-    // FIXME: SHould this be CreateSimpITE?
-    result = CreateNode(ITE, BBForm(form[0]), BBForm(form[1]), BBForm(form[2]));
-    break;
-
-  case AND: 
-  case OR: 
-  case NAND: 
-  case NOR: 
-  case IFF: 
-  case XOR:
-  case IMPLIES: {
-    ASTVec bbkids;		// bit-blasted children (formulas)
-
-    // FIXME: Put in fast exits for AND/OR/NAND/NOR/IMPLIES
-    ASTVec::const_iterator kids_end = form.end(); 
-    for (ASTVec::const_iterator it = form.begin(); it != kids_end; it++) {
-      bbkids.push_back(BBForm(*it));
-    }
-    result = CreateSimpForm(k, bbkids);
-    break;
-  }
-
-  case NEQ: {
-    ASTNode bbkid = BBForm(CreateNode(EQ, form.GetChildren()));
-    result = CreateSimpNot(bbkid);
-    break;
-  }
-
-  case EQ: {
-    // Common code for binary operations
-    // FIXME:  This ought to be in a semantic analysis phase.
-    const ASTNode left = BBTerm(form[0]);
-    const ASTNode right = BBTerm(form[1]);
-    if (left.Degree() != right.Degree()) {
-      cerr << "BBForm: Size mismatch" << endl << form[0] << endl << form[1] << endl;
-      FatalError("",ASTUndefined);
-    }
-    result = BBEQ(left.GetChildren(), right.GetChildren());
-    break;
-  }
-
-  case BVLE: 
-  case BVGE: 
-  case BVGT: 
-  case BVLT: 
-  case BVSLE:
-  case BVSGE:
-  case BVSGT:
-  case BVSLT: {
-    result = BBcompare(form);
-    break;
-  }
-  default:
-    FatalError("BBForm: Illegal kind: ", form);
-    break;
-  }
-
-  // cout << "================" << endl
-  // << "BBForm: " << form << endl
-  // << "----------------" << endl
-  // << "BBForm Result: " << result << endl;
-
-  return (BBFormMemo[form] = result);
-}
-  
-// Bit blast a sum of two equal length BVs.
-// Update sum vector destructively with new sum.
-void BeevMgr::BBPlus2(ASTVec& sum, const ASTVec& y, ASTNode cin)
-{
-//   cout << "Bitblasting plus.  Operand 1: " << endl;
-//   lpvec(sum);
-//   cout << endl << " operand 2: " << endl;
-//   lpvec(y);
-//   cout << endl << "carry: " << endl << cin << endl;
-
-
-  int n = sum.size();
-  // ASSERT: y.size() == x.size()
-  // FIXME: Don't bother computing i+1 carry, which is discarded.
-  for (int i = 0; i < n; i++) {
-    ASTNode nextcin = Majority(sum[i], y[i], cin); 
-    sum[i] = CreateSimpForm(XOR, CreateSimpForm(XOR, sum[i], y[i]), cin);
-    cin = nextcin;
-  }
-
-//   cout << "----------------" << endl << "Result: " << endl;
-//   lpvec(sum);
-//   cout << endl;
-
-}
-
-// Stores result - x in result, destructively
-void BeevMgr::BBSub(ASTVec& result, const ASTVec& y)
-{
-  ASTVec compsubtrahend  = BBNeg(y);
-  BBPlus2(result, compsubtrahend, ASTTrue);
-}
-
-// Add one bit
-ASTVec BeevMgr::BBAddOneBit(ASTVec& x, ASTNode cin)
-{
-  ASTVec result = ASTVec(0);
-  ASTVec::const_iterator itend = x.end();
-  for (ASTVec::const_iterator it = x.begin(); it < itend; it++) {
-    ASTNode nextcin = CreateSimpForm(AND, *it, cin); 
-    result.push_back(CreateSimpForm(XOR, *it, cin));
-    cin = nextcin;
-  }
-  // FIXME: unnecessary array copy on return?
-  return result;
-}
-
-// Increment bit-blasted vector and return result.
-ASTVec BeevMgr::BBInc(ASTVec& x)
-{
-  return BBAddOneBit(x, ASTTrue);
-}
-
-// Return formula for majority function of three bits.
-// Pass arguments by reference to reduce refcounting.
-ASTNode BeevMgr::Majority(const ASTNode& a, const ASTNode& b,const ASTNode& c)
-{
-  // Checking explicitly for constant a, b and c could
-  // be more efficient, because they are repeated in the logic.
-  if (ASTTrue == a) {
-    return CreateSimpForm(OR, b, c);
-  }
-  else if (ASTFalse == a) {
-    return CreateSimpForm(AND, b, c);
-  }
-  else if (ASTTrue == b) {
-    return CreateSimpForm(OR, a, c);
-  }
-  else if (ASTFalse == b) {
-    return CreateSimpForm(AND, a, c);
-  }
-  else if (ASTTrue == c) {
-    return CreateSimpForm(OR, a, b);
-  }
-  else if (ASTFalse == c) {
-    return CreateSimpForm(AND, a, b);
-  }
-  // there are lots more simplifications, but I'm not sure they're
-  // worth doing explicitly (e.g., a = b, a = ~b, etc.) 
-  else {
-    return
-      CreateSimpForm(OR,
-		     CreateSimpForm(AND, a, b),
-		     CreateSimpForm(AND, b, c),
-		     CreateSimpForm(AND, a, c));
-  }
-}
-
-
-// Bitwise complement
-ASTVec BeevMgr::BBNeg(const ASTVec& x)
-{
-  ASTVec result = ASTVec(0);		// FIXME: faster to preallocate n entries?
-  // Negate each bit.
-  ASTVec::const_iterator xend = x.end();
-  for (ASTVec::const_iterator it = x.begin(); it < xend; it++) {
-    result.push_back(CreateSimpNot(*it));
-  }
-  // FIXME: unecessary array copy when it returns?
-  return result;
-}
-
-// Compute unary minus
-ASTVec BeevMgr::BBUminus(const ASTVec& x)
-{
-  ASTVec xneg = BBNeg(x);
-  return BBInc(xneg);
-}
-
-// Multiply two bitblasted numbers
-ASTVec BeevMgr::BBMult(const ASTVec& x, const ASTVec& y)
-{
-  ASTVec ycopy(y);
-  ASTVec::const_iterator xend = x.end();
-  ASTVec::const_iterator xit = x.begin();
-  // start prod with first partial product.
-  // FIXME: This is unnecessary. Clean it up.
-  ASTVec prod = ASTVec(BBAndBit(y, *xit));
-  // start loop at next bit.
-  for(xit++; xit < xend; xit++) {
-    // shift first
-    BBLShift(ycopy);
-
-    if (ASTFalse == *xit) {
-      // If this bit is zero, the partial product will
-      // be zero.  No reason to add that in.
-      continue;
-    }
-
-    ASTVec pprod = BBAndBit(ycopy, *xit);
-    // accumulate in the product.
-    BBPlus2(prod, pprod, ASTFalse);
-  }
-  return prod;
-}
-
-// This implements a variant of binary long division.
-// q and r are "out" parameters.  rwidth puts a bound on the
-// recursion depth.
-void BeevMgr::BBDivMod(const ASTVec &y, const ASTVec &x, ASTVec &q, ASTVec &r, unsigned int rwidth)
-{
-  unsigned int width = y.size();
-  if (rwidth == 0) {
-    // When we have shifted the entire width, y is guaranteed to be 0.
-    q = BBfill(width, ASTFalse);
-    r = BBfill(width, ASTFalse);
-  }
-  else {
-    ASTVec q1, r1;
-    ASTVec yrshift1(y);
-    BBRShift(yrshift1);
-
-    // recursively divide y/2 by x.
-    BBDivMod(yrshift1, x, q1, r1, rwidth-1);
-
-    ASTVec q1lshift1(q1);
-    BBLShift(q1lshift1);
-
-    ASTVec r1lshift1(r1);
-    BBLShift(r1lshift1);
-    
-    ASTVec r1lshift1plusyodd = BBAddOneBit(r1lshift1, y[0]);
-    ASTVec rminusx(r1lshift1plusyodd);
-    BBSub(rminusx, x);
-
-    // Adjusted q, r values when when r is too large.
-    ASTNode rtoolarge = BBBVLE(x, r1lshift1plusyodd, false);
-    ASTVec ygtrxqval = BBITE(rtoolarge, BBInc(q1lshift1), q1lshift1);
-    ASTVec ygtrxrval = BBITE(rtoolarge, rminusx, r1lshift1plusyodd);
-
-    // q & r values when y >= x
-    ASTNode yeqx = BBEQ(y, x);
-    // *** Problem: the bbfill for qval is wrong.  Should be 1, not -1.
-    ASTVec one = BBfill(width, ASTFalse);
-    one[0] = ASTTrue;
-    ASTVec notylessxqval = BBITE(yeqx, one, ygtrxqval);
-    ASTVec notylessxrval = BBITE(yeqx, BBfill(width, ASTFalse), ygtrxrval);
-    // y < x <=> not x >= y.
-    ASTNode ylessx = CreateSimpNot(BBBVLE(x, y, false));
-    // final values of q and r
-    q = BBITE(ylessx, BBfill(width, ASTFalse), notylessxqval);
-    r = BBITE(ylessx, y, notylessxrval);
-  }
-}
-
-// build ITE's (ITE cond then[i] else[i]) for each i.
-ASTVec BeevMgr::BBITE(const ASTNode& cond, const ASTVec& thn, const ASTVec& els)
-{
-  // Fast exits.
-  if (ASTTrue == cond) {
-    return thn;
-  }
-  else if (ASTFalse == cond) {
-    return els;
-  }
-
-  ASTVec result(0);
-  ASTVec::const_iterator th_it_end = thn.end();
-  ASTVec::const_iterator el_it = els.begin();
-  for (ASTVec::const_iterator th_it = thn.begin(); th_it < th_it_end; th_it++, el_it++) {
-    result.push_back(CreateSimpForm(ITE, cond, *th_it, *el_it));
-  }
-  return result;
-}
-// AND each bit of vector y with single bit b and return the result.
-ASTVec BeevMgr::BBAndBit(const ASTVec& y, ASTNode b)
-{
-  ASTVec result(0); 
-
-  if (ASTTrue == b) {
-    return y;
-  }
-  // FIXME: put in fast exits when b is constant 0. 
-
-  ASTVec::const_iterator yend = y.end();
-  for(ASTVec::const_iterator yit = y.begin(); yit < yend; yit++) {
-    result.push_back(CreateSimpForm(AND, *yit, b));
-  }
-  return result;
-}
-
-
-// Workhorse for comparison routines.  This does a signed BVLE if is_signed
-// is true, else it's unsigned.  All other comparison operators can be reduced
-// to this by swapping args or complementing the result bit.
-// FIXME:  If this were done MSB first, it would enable a fast exit sometimes
-// when the MSB is constant, deciding the result without looking at the rest
-// of the bits.
-ASTNode BeevMgr::BBBVLE(const ASTVec& left, const ASTVec& right, bool is_signed)
-{
-  // "thisbit" represents BVLE of the suffixes of the BVs
-  // from that position .  if R < L, return TRUE, else if L < R
-  // return FALSE, else return BVLE of lower-order bits.  MSB is
-  // treated separately, because signed comparison is done by
-  // complementing the MSB of each BV, then doing an unsigned
-  // comparison.
-  ASTVec::const_iterator lit = left.begin();
-  ASTVec::const_iterator litend = left.end();
-  ASTVec::const_iterator rit = right.begin();
-  ASTNode prevbit = ASTTrue;
-  for ( ; lit  < litend-1; lit++, rit++) {
-    ASTNode neglit = CreateSimpNot(*lit);
-    ASTNode thisbit =
-      CreateSimpForm(OR,
-		 CreateSimpForm(AND,neglit,*rit), // TRUE if l < r
-		 CreateSimpForm(AND,
-			    CreateSimpForm(OR, neglit, *rit), // false if not equal
-			    prevbit)); // else prevbit
-    prevbit = thisbit;
-  }
-
-  // Handle MSB -- negate MSBs if signed comparison
-  // FIXME: make into refs after it's debugged.
-  ASTNode lmsb = *lit;
-  ASTNode rmsb = *rit;
-  if (is_signed) {
-    lmsb = CreateSimpNot(*lit);
-    rmsb = CreateSimpNot(*rit);
-  }
-
-  ASTNode neglmsb = CreateSimpNot(lmsb);
-  ASTNode msb =
-    CreateSimpForm(OR,
-	       CreateSimpForm(AND,neglmsb, rmsb), // TRUE if l < r
-	       CreateSimpForm(AND,
-			  CreateSimpForm(OR, neglmsb, rmsb), // false if not equal
-			  prevbit)); // else prevbit
-  return msb;
-}
-
-// Left shift by 1 within fixed field inserting zeros at LSB.
-// Writes result into first argument.
-// Fixme: generalize to n bits
-void BeevMgr::BBLShift(ASTVec& x)
-{
-  // left shift x (destructively) within width.
-  // loop backwards so that copy to self works correctly. (DON'T use STL insert!)
-  ASTVec::iterator xbeg = x.begin();
-  for(ASTVec::iterator xit = x.end()-1; xit > xbeg; xit--) {
-    *xit = *(xit-1);
-  }
-  *xbeg = ASTFalse;		// new LSB is zero.
-  // cout << "Shifted result" << endl;
-  // lpvec(x);
-}
-
-// Right shift by 1 within fixed field, inserting new zeros at MSB.
-// Writes result into first argument.
-// Fixme: generalize to n bits.
-void BeevMgr::BBRShift(ASTVec& x)
-{
-  ASTVec::iterator xend = x.end() - 1;
-  ASTVec::iterator xit = x.begin();
-  for( ; xit < xend; xit++) {
-    *xit = *(xit+1);
-  }
-  *xit = ASTFalse;		// new MSB is zero.
-}
-
-
-// Return bit-blasted form for BVLE, BVGE, BVGT, SBLE, etc. 
-ASTNode BeevMgr::BBcompare(const ASTNode& form) {
-  const ASTNode lnode = BBTerm(form[0]);
-  const ASTNode rnode = BBTerm(form[1]);
-  const ASTVec& left = lnode.GetChildren();
-  const ASTVec& right = rnode.GetChildren();
-
-  //const ASTVec& left = BBTerm(form[0]).GetChildren();
-  //const ASTVec& right = BBTerm(form[1]).GetChildren();
-
-  Kind k = form.GetKind();
-  switch(k) {
-  case BVLE: { return BBBVLE(left, right, false); break; }
-  case BVGE: { return BBBVLE(right, left, false); break; }
-  case BVGT: { return CreateSimpNot(BBBVLE(left, right, false)); break; }
-  case BVLT: { return CreateSimpNot(BBBVLE(right, left, false)); break; }
-  case BVSLE: { return BBBVLE(left, right, true); break; }
-  case BVSGE: { return BBBVLE(right, left, true); break; }
-  case BVSGT: { return CreateSimpNot(BBBVLE(left, right, true)); break; }
-  case BVSLT: { return CreateSimpNot(BBBVLE(right, left, true)); break; }
-  default:
-    cerr << "BBCompare: Illegal kind" << form << endl;    
-    FatalError("",ASTUndefined);
-  }
-  return ASTUndefined;
-}
-
-
-// return a vector with n copies of fillval
-ASTVec BeevMgr::BBfill(unsigned int width, ASTNode fillval)
-{
-  ASTVec zvec(width, fillval);
-  return zvec;
-}
-
-ASTNode BeevMgr::BBEQ(const ASTVec& left, const ASTVec& right)
-{
-  ASTVec andvec;
-  ASTVec::const_iterator lit = left.begin();
-  ASTVec::const_iterator litend = left.end();
-  ASTVec::const_iterator rit = right.begin();
-  
-  if(left.size() > 1) {
-    for(; lit != litend; lit++, rit++) {
-      ASTNode biteq = CreateSimpForm(IFF, *lit, *rit);
-      // fast path exit
-      if (biteq == ASTFalse) {
-	return ASTFalse;
-      }
-      else {
-	andvec.push_back(biteq);
-      }
-    }
-    ASTNode n = CreateSimpForm(AND, andvec);  
-    return n;
-  }
-  else
-    return CreateSimpForm(IFF,*lit,*rit);
-}
-} // BEEV namespace
diff --git a/stp/AST/Makefile b/stp/AST/Makefile
deleted file mode 100644
index c3b54672..00000000
--- a/stp/AST/Makefile
+++ /dev/null
@@ -1,19 +0,0 @@
-#===-- stp/AST/Makefile ------------------------------------*- Makefile -*--===#
-#
-#                     The KLEE Symbolic Virtual Machine
-#
-# This file is distributed under the University of Illinois Open Source
-# License. See LICENSE.TXT for details.
-#
-#===------------------------------------------------------------------------===#
-
-LEVEL=../..
-
-LIBRARYNAME=stp_AST
-DONT_BUILD_RELINKED=1
-BUILD_ARCHIVE=1
-
-include $(LEVEL)/Makefile.common
-
-# HACK: Force -Wno-deprecated for ext container use.
-CXX.Flags += -Wno-deprecated
diff --git a/stp/AST/STLport_config.h b/stp/AST/STLport_config.h
deleted file mode 100644
index 9b7bc14f..00000000
--- a/stp/AST/STLport_config.h
+++ /dev/null
@@ -1,20 +0,0 @@
-/********************************************************************
- * AUTHORS: Vijay Ganesh, David L. Dill
- *
- * BEGIN DATE: November, 2005
- *
- * LICENSE: Please view LICENSE file in the home dir of this Program
- ********************************************************************/
-// -*- c++ -*-
-
-// STLport debug checking, if we use STLport threads flag is to get
-// rid of link errors, since iostreams compiles with threads.  alloc
-// and uninitialized are extra checks Later on, if used with Purify or
-// Valgrind, may want to set flags to prevent reporting of false
-// leaks.  For some reason, _STLP_THREADS works on the command line
-// but not here (?)
-#define _STLP_THREADS
-#define _STLP_DEBUG 1
-#define _STLP_DEBUG_LEVEL _STLP_STANDARD_DBG_LEVEL 
-#define _STLP_DEBUG_ALLOC 1
-#define _STLP_DEBUG_UNINITIALIZED 1
diff --git a/stp/AST/SimpBool.cpp b/stp/AST/SimpBool.cpp
deleted file mode 100644
index 67f9825d..00000000
--- a/stp/AST/SimpBool.cpp
+++ /dev/null
@@ -1,408 +0,0 @@
-/********************************************************************
- * AUTHORS: Vijay Ganesh, David L. Dill
- *
- * BEGIN DATE: April, 2006
- *
- * LICENSE: Please view LICENSE file in the home dir of this Program
- ********************************************************************/
-
-// -*- c++ -*-
-
-// Simplifying create methods for Boolean operations.
-// These are only very simple local simplifications.
-
-// This is somewhat redundant with Vijay's simplifier code.  They
-// need to be merged.
-// FIXME: control with optimize flag.
-
-static bool _trace_simpbool = 0;
-static bool _disable_simpbool = 0;
-
-#include "AST.h"
-
-// SMTLIB experimental hack.  Try allocating a single stack here for
-// children to reduce growing of vectors.
-//BEEV::ASTVec child_stack;
-
-namespace BEEV {
-
-  ASTNode BeevMgr::CreateSimpForm(Kind kind, ASTVec &children = _empty_ASTVec) {
-    if (_disable_simpbool) {
-      return CreateNode(kind, children);
-    }
-    else {
-      switch (kind) {
-      case NOT: return CreateSimpNot(children[0]); break; 
-      case AND: return CreateSimpAndOr(1, children); break; 
-      case OR: return CreateSimpAndOr(0, children); break;
-      case NAND: return CreateSimpNot(CreateSimpAndOr(1, children)); break;
-      case NOR: return CreateSimpNot(CreateSimpAndOr(0, children)); break;
-      case IFF: {
-	// Not sure children can ever be empty, but what the heck.
-	//	if (children.size() == 0) {
-	//	  return ASTTrue;
-	//	}
-	// Convert IFF to XOR ASAP.  IFF is not associative, so this makes
-	// flattening much easier.
-	children[0] = CreateSimpNot(children[0]);
-	return CreateSimpXor(children); break;
-      }
-      case XOR: 
-	return CreateSimpXor(children); break;
-	// FIXME: Earlier, check that this only has two arguments
-      case IMPLIES: return CreateSimpAndOr(0, CreateSimpNot(children[0]), children[1]); break;
-      case ITE: return CreateSimpFormITE(children[0], children[1], children[2]);
-      default: return CreateNode(kind, children);
-      }
-    }
-  }
-
-  // specialized versions
-  
-  ASTNode BeevMgr::CreateSimpForm(Kind kind,
-				  const ASTNode& child0) {
-    ASTVec children;
-    //child_stack.clear();	// could just reset top pointer.
-    children.push_back(child0);
-    //child_stack.push_back(child0);
-    return CreateSimpForm(kind, children);
-    //return CreateSimpForm(kind, child_stack);
-  }
-  
-  ASTNode BeevMgr::CreateSimpForm(Kind kind,
-				  const ASTNode& child0,
-				  const ASTNode& child1) {
-    ASTVec children;
-    //child_stack.clear();	// could just reset top pointer.
-    children.push_back(child0);
-    //child_stack.push_back(child0);
-    children.push_back(child1);
-    //child_stack.push_back(child1);
-    return CreateSimpForm(kind, children);
-    //return CreateSimpForm(kind, child_stack);
-  }
-  
-  
-  ASTNode BeevMgr::CreateSimpForm(Kind kind,
-				  const ASTNode& child0,
-				  const ASTNode& child1,
-				  const ASTNode& child2) {
-    ASTVec children;
-    //child_stack.clear();	// could just reset top pointer.
-    children.push_back(child0);
-    //child_stack.push_back(child0);
-    children.push_back(child1);
-    //child_stack.push_back(child1);
-    children.push_back(child2);
-    //child_stack.push_back(child2);
-    return CreateSimpForm(kind, children);
-    //return CreateSimpForm(kind, child_stack);
-  }
-    
-  ASTNode BeevMgr::CreateSimpNot(const ASTNode& form) {
-    Kind k = form.GetKind();
-    switch (k) {
-    case FALSE: { return ASTTrue; }
-    case TRUE: { return ASTFalse; }
-    case NOT: { return form[0]; } // NOT NOT cancellation
-    case XOR: {
-      // Push negation down in this case.
-      // FIXME: Separate pre-pass to push negation down?
-      // CreateSimp should be local, and this isn't.  
-      // It isn't memoized.  Arg.
-      ASTVec children = form.GetChildren();
-      children[0] = CreateSimpNot(children[0]);
-      return CreateSimpXor(children);
-    }
-    default: { return CreateNode(NOT, form); }
-    }
-  }
-
-  // I don't think this is even called, since it called
-  // CreateSimpAndOr instead of CreateSimpXor until 1/9/07 with no
-  // ill effects.  Calls seem to go to the version that takes a vector
-  // of children.
-  ASTNode BeevMgr::CreateSimpXor(const ASTNode& form1, const ASTNode& form2) {
-    ASTVec children;
-    children.push_back(form1);
-    children.push_back(form2);
-    return CreateSimpXor(children);
-  }
-
-
-  ASTNode BeevMgr::CreateSimpAndOr(bool IsAnd, const ASTNode& form1, const ASTNode& form2) {
-    ASTVec children;
-    children.push_back(form1);
-    children.push_back(form2);
-    return CreateSimpAndOr(IsAnd, children);
-  }
-
-  ASTNode BeevMgr::CreateSimpAndOr(bool IsAnd, ASTVec &children) {
-
-    if (_trace_simpbool) {
-      cout << "========" << endl << "CreateSimpAndOr " << (IsAnd ? "AND " : "OR ") ;
-      lpvec(children);
-      cout << endl;
-    }
-
-    ASTVec new_children;
-
-    // sort so that identical nodes occur in sequential runs, followed by
-    // their negations.
-
-    SortByExprNum(children);
-    
-    ASTNode annihilator = (IsAnd ? ASTFalse : ASTTrue);
-    ASTNode identity = (IsAnd ? ASTTrue : ASTFalse);
-
-    ASTNode retval;
-
-    ASTVec::const_iterator it_end = children.end();
-    ASTVec::const_iterator next_it;
-    for(ASTVec::const_iterator it = children.begin(); it != it_end; it = next_it) {
-      next_it = it + 1;
-      bool nextexists = (next_it < it_end);
-
-      if (*it == annihilator) {
-	retval = annihilator;
-	if (_trace_simpbool) {
-	  cout << "returns " << retval << endl;
-	}
-	return retval;
-      }
-      else if (*it == identity) {
-	// just drop it
-      }
-      else if (nextexists && (*next_it == *it)) {
-	// drop it
-	//	cout << "Dropping [" << it->GetNodeNum() << "]" << endl;
-      }
-      else if (nextexists && (next_it->GetKind() == NOT) && ((*next_it)[0] == *it)) {
-	// form and negation -- return FALSE for AND, TRUE for OR.
-	retval = annihilator;
-	// cout << "X and/or NOT X" << endl; 
-	if (_trace_simpbool) {
-	  cout << "returns " << retval << endl;
-	}
-	return retval;
-      }
-      else {
-	// add to children
-	new_children.push_back(*it);
-      }
-    }
-
-    // If we get here, we saw no annihilators, and children should
-    // be only the non-True nodes.
-    if (new_children.size() < 2) {
-      if (0 == new_children.size()) {
-	retval = identity;
-      }
-      else {
-	// there is just one child
-	retval = new_children[0];
-      }
-    }
-    else {
-      // 2 or more children.  Create a new node.
-      retval = CreateNode(IsAnd ? AND : OR, new_children);
-    }
-    if (_trace_simpbool) {
-      cout << "returns " << retval << endl;
-    }
-    return retval;
-  }
-
-
-  // Constant children are accumulated in "accumconst".  
-  ASTNode BeevMgr::CreateSimpXor(ASTVec &children) {
-
-    if (_trace_simpbool) {
-      cout << "========" << endl
-	   << "CreateSimpXor ";
-      lpvec(children);
-      cout << endl;
-    }
-
-    // Change this not to init to children if flattening code is present.
-    // ASTVec flat_children = children;		// empty vector
-
-    ASTVec flat_children;		// empty vector
-
-    ASTVec::const_iterator it_end = children.end();
-
-    if (xor_flatten) {
-
-      bool fflag = 0;		// ***Temp debugging
-      
-      // Experimental flattening code.
-      
-      for(ASTVec::iterator it = children.begin(); it != it_end; it++) {
-	Kind ck = it->GetKind();
-	const ASTVec &gchildren = it->GetChildren();
-	if (XOR == ck) {
-	  fflag = 1;
-	  // append grandchildren to children
-	  flat_children.insert(flat_children.end(), gchildren.begin(), gchildren.end());
-	}
-	else {
-	  flat_children.push_back(*it);
-	}
-      }
-      
-      if (_trace_simpbool && fflag) {
-	cout << "========" << endl;
-	cout << "Flattening: " << endl;
-	lpvec(children);
-	
-	cout << "--------" << endl;
-	cout << "Flattening result: " << endl;
-	lpvec(flat_children);
-      }
-    }
-    else {
-      flat_children = children;
-    }
-      
-
-    // sort so that identical nodes occur in sequential runs, followed by
-    // their negations.
-    SortByExprNum(flat_children);
-
-    ASTNode retval;
-
-    // This is the C Boolean value of all constant args seen.  It is initially
-    // 0.  TRUE children cause it to change value.
-    bool accumconst = 0;
-
-    ASTVec new_children;
-
-    it_end = flat_children.end();
-    ASTVec::iterator next_it;
-    for(ASTVec::iterator it = flat_children.begin(); it != it_end; it++) {
-      next_it = it + 1;
-      bool nextexists = (next_it < it_end);
-
-      if (ASTTrue == *it) {
-	accumconst = !accumconst;
-      }
-      else if (ASTFalse == *it) {
-	// Ignore it
-      }
-      else if (nextexists && (*next_it == *it)) {
-	// x XOR x = FALSE.  Skip current, write "false" into next_it
-	// so that it gets tossed, too.
-	*next_it = ASTFalse;
-      }
-      else if (nextexists && (next_it->GetKind() == NOT) && ((*next_it)[0] == *it)) {
-	// x XOR NOT x = TRUE.  Skip current, write "true" into next_it
-	// so that it gets tossed, too.
-	*next_it = ASTTrue;
-      }
-      else if (NOT == it->GetKind()) {
-	// If child is (NOT alpha), we can flip accumconst and use alpha.
-	// This is ok because (NOT alpha) == TRUE XOR alpha
-	accumconst = !accumconst;
-	// CreateSimpNot just takes child of not.
-	new_children.push_back(CreateSimpNot(*it));
-      }
-      else {
-	new_children.push_back(*it);
-      }
-    }
-
-    // Children should be non-constant.
-    if (new_children.size() < 2) {
-      if (0 == new_children.size()) {
-	// XOR(TRUE, FALSE) -- accumconst will be 1.
-	if (accumconst) {
-	  retval = ASTTrue;
-	}
-	else {
-	  retval = ASTFalse;
-	}
-      }
-      else {
-	// there is just one child
-	// XOR(x, TRUE) -- accumconst will be 1.
-	if (accumconst) {
-	  retval =  CreateSimpNot(new_children[0]);
-	}
-	else {
-	  retval = new_children[0];
-	}
-      }
-    }
-    else {
-      // negate first child if accumconst == 1
-      if (accumconst) {
-	new_children[0] = CreateSimpNot(new_children[0]);
-      }
-      retval = CreateNode(XOR, new_children);
-    }
-
-    if (_trace_simpbool) {    
-      cout << "returns " << retval << endl;
-    }
-    return retval;
-  }
-
-  // FIXME:  How do I know whether ITE is a formula or not?
-  ASTNode BeevMgr::CreateSimpFormITE(const ASTNode& child0,
-				     const ASTNode& child1,
-				     const ASTNode& child2) {
-
-    ASTNode retval;
-    
-    if (_trace_simpbool) {
-      cout << "========" << endl << "CreateSimpFormITE "
-	   << child0 
-	   << child1 
-	   << child2 << endl;
-    }
-
-    if (ASTTrue == child0) {
-      retval = child1;
-    }
-    else if (ASTFalse == child0) {
-      retval = child2;
-    }
-    else if (child1 == child2) {
-      retval = child1;
-    }    
-    // ITE(x, TRUE, y ) == x OR y
-    else if (ASTTrue == child1) {
-      retval = CreateSimpAndOr(0, child0, child2);
-    }
-    // ITE(x, FALSE, y ) == (!x AND y)
-    else if (ASTFalse == child1) {
-      retval = CreateSimpAndOr(1, CreateSimpNot(child0), child2); 
-    }
-    // ITE(x, y, TRUE ) == (!x OR y)
-    else if (ASTTrue == child2) {
-      retval = CreateSimpAndOr(0, CreateSimpNot(child0), child1); 
-    }
-    // ITE(x, y, FALSE ) == (x AND y)
-    else if (ASTFalse == child2) {
-      retval = CreateSimpAndOr(1, child0, child1); 
-    }
-    // ITE (x, !y, y) == x XOR y
-//     else if (NOT == child1.GetKind() && (child1[0] == child2)) {
-//       retval = CreateSimpXor(child0, child2);
-//     }
-//     // ITE (x, y, !y) == x IFF y.  I think other cases are covered
-//     // by XOR/IFF optimizations
-//     else if (NOT == child2.GetKind() && (child2[0] == child1)) {
-//       retval = CreateSimpXor(CreateSimpNot(child0), child2);
-//     }
-    else {
-      retval = CreateNode(ITE, child0, child1, child2);
-    }
-
-    if (_trace_simpbool) {
-      cout << "returns " << retval << endl;
-    }
-
-    return retval;
-  }
-} // BEEV namespace
diff --git a/stp/AST/ToCNF.cpp b/stp/AST/ToCNF.cpp
deleted file mode 100644
index 2a18b3f5..00000000
--- a/stp/AST/ToCNF.cpp
+++ /dev/null
@@ -1,506 +0,0 @@
-/********************************************************************
- * AUTHORS: David L. Dill, Vijay Ganesh 
- *
- * BEGIN DATE: November, 2005
- *
- * LICENSE: Please view LICENSE file in the home dir of this Program
- ********************************************************************/
-// -*- c++ -*-
-
-// THEORY: This code translates an arbitrary Boolean DAG, generated by
-// the BitBlast.cpp, to an equi-satisfiable CNF formula.  There are
-// four kinds of variables in the CNF formula: (1) propositional
-// variables from the original formula; (2) BVGETBIT formulas from the
-// original formula (a precondition is that the BVGETBIT can only be
-// applied to bitvector-valued variables, array reads, or
-// uninterpreted functions); (3) TRUE; or (4) representative variables
-// (see below).  Each literal in the CNF formula is one of these or
-// its negation.  
-
-// It is convenient (though not perfectly efficient) to be able to add
-// TRUE and FALSE constants to clauses, which is not allowed in CNF.
-// So, there is a "dummy variable" representing TRUE, which is used in
-// its place (so FALSE is represented by the negation of the dummy
-// var).  The CNF formula has a unit clause containing this dummy
-// variable, so that any satisfying assignment must make the dummy var
-// TRUE.
-
-// Every sub-formula of the input formula has a "representative
-// literal."  A truth assignment satisfies the CNF formula iff the
-// restriction of that assignment to the original variables satisfies
-// the original formula, AND the rep lits have the same truth values
-// as the subformulas they represent in the original formula.  In the
-// trivial cases, the representative literal is the input variable, or
-// dummy true var, or its negation.  Representative literals may be
-// negated variables -- essentially, only AND formulas are translated,
-// and everything else is handled by rewriting or negating formulas.
-// The representative for (NOT alpha) is the negation of the
-// representative for alpha.
-
-// The translation is performed by ToCNF_int, which traverses the original
-// formula.  ToCNF adds clauses that constrain the representative variables
-// to be equal to the truth values of the formulas they represent.
-// ToCNF always returns a literal whose value must be equivalent to the formula
-// it translated.  In trivial cases, this literal is a literal from the original
-// formula, or the dummy true/false literals.  If the formula is of the form
-// (not alpha), ToCNF_int negates the literal representing alpha (which may
-// itself be a negative literal) and returns it.  Otherwise, ToCNF_int assigns
-// a new rep var, adds the clauses, and returns the new var.  ToCNF_int is
-// memoized so that it doesn't assign more than one variable to a subformula,
-// and to prevent exponential numbers of redundant visits to shared subformulas.
-
-// In reality, only AND/OR/NOT formulas are translated directly.  Everything
-// else (XOR, IFF, IMPLIES) is rewritten on-the-fly into these forms.  I
-// could have done that in bit-blasting, but I thought that, in the future,
-// we might be able to translate these operations differently in different
-// contexts to optimize the CNF formula.
-
-// FIXME: Inspection of the clauses is kind of horrifying.  In
-// addition to true/false, there are duplicate literals and duplicate
-// clauses all over the place.
-#include "AST.h"
-static bool CNF_trace = false;
-namespace BEEV {
-/**  Statistics class.  Total number of variables is best tracked in
-     ToSAT.  Number of clauses is just cll.size() */
-
-class CNFstats {
-public:
-  int _num_new_rep_vars;
-  int _num_clauses;
-  
-  // constructor
-  CNFstats() : _num_new_rep_vars(0), _num_clauses(0) {}
-
-  void printStats() {
-    if(stats) {
-      cout << "ToCNF statistics:" << endl;
-      cout << "Number of new representative variables: "
-	   << _num_new_rep_vars << endl;
-      cout << "Number of new clauses: "
-	   << _num_clauses << endl;
-    }
-  }
-
-};
-
-
-/** This class contains private data and function members for the
-    CNF conversion */
-class CNFMgr {
-
-  friend class BeevMgr;
-
-public:    
-
-  // Needed in the body of BeevMgr::ToCNF.  It's not visible outside
-  // this file, though.
-  ASTNode dummy_true_var;
-
-  // CNF Pre-pass
-  ASTNodeMap ToCNFPrePassMemo;
-
-  // CNF Memo Table.
-  ASTNodeMap CNFMemo;
-
-
-private:
-
-  // Pointer back to BeevMgr with the node tables, etc.
-  BeevMgr *bm;
-  
-  // For ToCNF conversion.  This holds a dummy variable representing
-  // "True".  It is added as a unit clause, so that it will be assigned
-  // to true and propagated immediately by any CNF solver.
-
-  ASTNode dummy_false_var;	// not of dummy_true_var
-
-  CNFstats stats;
-
-  // constructor
-  CNFMgr(BeevMgr *bmgr)
-  {
-    bm = bmgr;
-
-    // Dummy variable so TRUE can be a literal.
-    dummy_true_var = bm->CreateSymbol("*TrueDummy*");
-    dummy_false_var = bm->CreateSimpNot(dummy_true_var);
-  }
-  
-  // Returns true iff result has been memoized.
-  // if it returns true, result is returned in by-ref parameter "result"
-  // Consider just putitng this in-line.
-  bool CNFIsMemoized(ASTNode &form, ASTNode &result)
-  {
-    ASTNodeMap::iterator it = CNFMemo.find(form);
-    if (it != CNFMemo.end()) {
-      result = it->second;  //already there. Just return it.
-      return true;
-    }
-    else {
-      return false;
-    }
-  }
-
-
-  // Convert a big XOR to a bunch of AND/ORs.  Assumes subformulas have
-  // already been converted.
-  ASTNode convertXORs(ASTVec children)
-  {
-    ASTNode accum = children[0];
-    ASTVec::iterator itend = children.end();
-    for (ASTVec::iterator it = children.begin()+1; it < itend; it++) {
-      // a XOR b -> (a | b) & (!a | !b)
-
-      // For each XOR node with k children, creates approximately
-      // 5*(k-1) nodes. AND + 2 OR + 2 NOT.
-
-      ASTNode or1 = bm->CreateNode(OR, accum, *it);
-      ASTNode or2 = bm->CreateNode(OR, bm->CreateSimpNot(accum), bm->CreateSimpNot(*it));
-      accum = bm->CreateNode(AND, or1, or2);
-      
-    }
-    
-    return accum;
-  }
-
-
-  // Do preliminary transformations on bitblasted formula to make 
-  // CNF conversion easier.
-  // Converts XORs to AND/OR form.
-  ASTNode ToCNFPrePass(const ASTNode &form)
-  {
-
-    // Check memo table
-    ASTNodeMap::iterator mem_it = ToCNFPrePassMemo.find(form);
-    if (mem_it != ToCNFPrePassMemo.end()) {
-      return mem_it->second;
-    }
-    
-    ASTNode result;
-
-    ASTVec new_children;
-    ASTVec::const_iterator endit = form.end();
-    for (ASTVec::const_iterator it = form.begin(); it != endit; it++) {
-      ASTNode ch = ToCNFPrePass(*it);
-      new_children.push_back(ch);
-    }
-
-    Kind k = form.GetKind();
-
-    switch (k) {
-    case FALSE: 
-    case TRUE:
-    case SYMBOL: 
-    case BVGETBIT: {
-      result = form;
-      break;
-    }
-    case XOR: {
-      // convertXORs can only be called once per XOR node.
-      result = convertXORs(new_children);
-
-      // cout << "convertXORs num args: "  << new_children.size() << endl;
-      // temporary node for node count.
-      // ASTNode tmp = bm->CreateNode(XOR, new_children );
-      // cout << "convertXORs size of [" << form.GetNodeNum() << "] " << bm->NodeSize(form, true) << endl;
-      // cout << "convertXORs before size: " << bm->NodeSize(tmp, true) << endl;
-      // cout << "convertXORs after size: " << bm->NodeSize(result, true) << endl;
-      break;
-    }
-    default: {
-      // Be cautious about using CreateSimpForm -- It makes big xors!
-      result = bm->CreateNode(k, new_children);
-    }
-    }
-
-//     cout << "================" << endl
-// 	 << "ToCNFPrePass:" << form << endl
-// 	 << "----------------" << endl
-// 	 << "ToCNFPrePass Result:" << result << endl;
-    
-    return (ToCNFPrePassMemo[form] = result);
-    
-  }
-
-  // Memoize and return formula value
-  ASTNode CNFMemoize(ASTNode& form, ASTNode result)
-  {
-    CNFMemo[form] = result;
-    return result;    
-  }
-
- 
-  // Create a representative variable for an original formula.
-  // The convention is that the variable will have the same truth
-  // value as the expression numbered "num."  
-  ASTNode RepLit(const char *name, int exprnum)
-  {
-    // FIXME: can this be done more efficiently with string type?
-    ostringstream oss;
-    oss << name << "{" << exprnum << "}";
-    ASTNode t = bm->CreateSymbol(oss.str().c_str());
-
-    // Track how many we're generating.
-    stats._num_new_rep_vars++;
-    
-    //ASTNode is of type BOOLEAN <==> ((indexwidth=0)&&(valuewidth=0))
-    t.SetIndexWidth(0);
-    t.SetValueWidth(0);
-    return t;
-  }
-
-  // Handle the cases where it's necessary to do n children.
-  // This code translates ANDs, and converts NAND, NOR, OR by negating
-  // the inputs or outputs of the AND.
-  ASTNode ToCNF_AndLike(Kind k, BeevMgr::ClauseList& cll, ASTNode form)
-  {  
-    // Build vectors of positive and negative rep lits for children
-    ASTVec kidlits(0);
-    ASTVec negkidlits(0);
-    ASTVec::const_iterator kids_end = form.end();
-    for (ASTVec::const_iterator it = form.begin(); it != kids_end; it++) {
-      ASTNode kidreplit = ToCNF_int(cll, *it);
-      kidlits.push_back(kidreplit);
-      negkidlits.push_back(bm->CreateSimpNot(kidreplit));
-    }
-    
-    ASTNode replit;
-    // translate the AND, negating inputs as appropriate.
-    if (k == OR || k == NOR) {
-      replit = ToCNF_AND(cll, form.GetNodeNum(), negkidlits, kidlits);
-    }
-    else {
-      replit = ToCNF_AND(cll, form.GetNodeNum(), kidlits, negkidlits);
-    }
-    
-    // Reduce NAND/OR to AND by negating result.
-    if (k == NAND || k == OR) {
-      return CNFMemoize(form, bm->CreateSimpNot(replit));
-    }
-    else {
-      return CNFMemoize(form, replit);
-    }
-  }
-
-  ASTNode ToCNF_AND(BeevMgr::ClauseList& cll, int nodenum, ASTVec& kidlits, ASTVec& negkidlits)
-  {
-    // Translate an AND, given rep lits for children
-    // Build clauses for (replit <-> a AND b AND c)
-
-    ASTNode replit = RepLit("cnf", nodenum);
-    ASTNode notreplit = bm->CreateSimpNot(replit);
-
-    if (CNF_trace) {
-      cout << "Translating AND" << endl << "-----------------------" << endl
-	   << "Rep lit =" <<  replit << endl
-	   << "-----------------------";
-    }
-
-    // (a AND b AND c -> replit) ==   (~a OR ~b OR ~c OR replit)
-    BeevMgr::ClausePtr clp = new ASTVec(negkidlits);
-    clp->push_back(replit);
-
-    if (CNF_trace) {
-      LispPrintVec(cout, *clp, 0);
-      cout << endl << "-----------------------" << endl;
-    }
-
-    cll.push_back(clp);
-
-    // (replit -> (a AND b AND c)) == 
-    //     (~replit OR a) AND (~replit OR b) AND (~replit OR c)
-    ASTVec::const_iterator kidlits_end = kidlits.end();
-    for (ASTVec::iterator it = kidlits.begin(); it != kidlits_end; it++) {
-      clp = new ASTVec();
-      clp->push_back(notreplit);
-      clp->push_back(*it);
-
-      if (CNF_trace) {
-	LispPrintVec(cout, *clp, 0);
-	cout << endl << "-----------------------" << endl;
-      }
-
-      cll.push_back(clp);
-    }
-
-    return replit;
-  }
-
-public:
-   
-  /** Builds clauses globally and returns a literal.
-      The literal can be a leaf from the expression, or a rep var
-      made up to represent the subexpression. */
-  ASTNode ToCNF_int(BeevMgr::BeevMgr::ClauseList& cll, ASTNode form) {
-    // FIXME: assert indexwidth= 0, valuewidth = 1
-
-    // FIXME:  rewriting is top-down, which is not efficient.
-    // It rewrites the top node of the tree, then does the children.
-    // Either rewrite in a separate pass, or translate children
-    // before rewriting somehow (might require handling rep lits
-    // as though they were real lits, which is probably ok).
-    
-    // Return memoized value if seen before.
-    ASTNode result;
-    Kind k = form.GetKind();
-
-    if (CNFIsMemoized(form, result)) {
-      return result;
-    }
-
-    switch (k) {
-      // handle the trivial cases here.  If none apply, call the
-      // heavy-duty function.  If a constant or literal, just return
-      // without creating a clause.
-    case FALSE: {
-      result = dummy_false_var;
-      break;
-    }
-    case TRUE: {
-      result =  dummy_true_var;
-      break;
-    }
-    case SYMBOL: 
-    case BVGETBIT: {
-      result = form;
-      break;
-    }
-      
-    case NOT: {
-	ASTNode replit = ToCNF_int(cll, form[0]);
-	result = bm->CreateSimpNot(replit);
-      break;
-    }
-      
-      // For these, I can't think of anything better than expanding into ANDs/ORs
-    case ITE: {
-      // (ite a b c) == (~a OR b) AND (a OR c)
-      ASTNode l = bm->CreateNode(OR, bm->CreateSimpNot(form[0]), form[1]);
-      ASTNode r = bm->CreateNode(OR, form[0], form[2]);
-      ASTNode andor = bm->CreateNode(AND, l, r);
-      if (CNF_trace) {
-	cout << "Rewriting " << form << endl
-	     << "to" << andor << endl
-	     << "-------------------" << endl;
-      }
-      result = ToCNF_int(cll, andor);
-      break;
-    }
-    case IMPLIES: {
-      // Just rewrite into (~a OR b)
-      ASTNode l = bm->CreateSimpNot(form[0]);
-      ASTNode andor = bm->CreateNode(OR, l, form[1]);
-      if (CNF_trace) {
-	cout << "Rewriting " << form << endl
-	     << "to" << andor << endl
-	     << "-------------------" << endl;
-      }
-      result = ToCNF_int(cll, andor);
-      break;
-    }
-    case XOR: {
-      FatalError("ToCNF_int: XORs should have been converted to AND/OR by this point.");
-      break;
-    }
-
-    case IFF: {
-      FatalError("BitBlaster failed to eliminate all IFFs.");
-      break;
-    }
-    
-    case AND:
-    case OR:
-    case NOR:
-    case NAND: {
-      result = ToCNF_AndLike(k, cll, form);
-      break;
-    }
-    default:
-      cerr << "ToCNF: can't handle this kind: " << k << endl;
-      FatalError("");
-    }
-
-    if (CNF_trace) {
-      cout << "ToCNF_int: Literal " << result << " represents formula " <<
-	form << endl << "---------------" << endl;
-    }
-
-    return CNFMemoize(form, result);
-  } //end of ToCNF_int()
-
-
-}; // end of CNFMgr class
-
-  // These are the bodies of functions in the BeevMgr that are part of
-  // the public interface.
-
-  // Debug printing function.
-  void BeevMgr::PrintClauseList(ostream& os, BeevMgr::ClauseList& cll)
-  {
-    int num_clauses = cll.size();
-    os << "Clauses: " << endl << "=========================================" << endl;
-    for(int i=0; i < num_clauses; i++) {
-      os << "Clause " << i << endl
-	 << "-------------------------------------------" << endl;
-      LispPrintVec(os, *cll[i], 0);
-      os << endl
-	 << "-------------------------------------------" << endl;
-    }
-  }
-
-  void BeevMgr::DeleteClauseList(BeevMgr::ClauseList *cllp)
-  {
-    BeevMgr::ClauseList::const_iterator iend = cllp->end();
-    for (BeevMgr::ClauseList::const_iterator i = cllp->begin(); i < iend; i++) {
-      delete *i;
-    }
-    delete cllp;
-  }
-
-  // Top level conversion function
-  BeevMgr::ClauseList *BeevMgr::ToCNF(const ASTNode& form) 
-  {
-
-    // FIXME: This is leaked as well.
-    CNFMgr *cm = new CNFMgr(this);
-   
-    // Prepass
-    ASTNode form1 = cm->ToCNFPrePass(form);
-
-    // cout << "Number of nodes after ToCNFPrePass" << NodeSize(form1, true) << endl;
-
-    // cout << "ToCNF: After ToCNFPrePass" << form1 << endl;
-
-    // FIXME: Assert CNFMemo is empty.
-
-    // The clause list we will be building up.
-    // FIXME: This is never freed.
-    ClauseList *cllp = new ClauseList();
-
-    BeevMgr::ClausePtr dummy_true_unit_clause = new ASTVec();
-    dummy_true_unit_clause->push_back(cm->dummy_true_var);
-    cllp->push_back(dummy_true_unit_clause);
-
-    // This is where the translation happens.
-    ASTNode toplit = cm->ToCNF_int(*cllp, form1);
-
-    // Add the top literal as a unit clause, since it must
-    // be true when original formula is satsfied.
-    BeevMgr::ClausePtr clp = new ASTVec(0);
-    clp->push_back(toplit);
-    cllp->push_back(clp);
-
-    cm->stats._num_clauses = cllp->size();
-    cm->stats.printStats();
-
-    RepLitMap = cm->CNFMemo;	// Save memo table for debugging (DD 1/13/07).
-
-    cm->CNFMemo.clear();   // Important to do this so nodes get freed.
-
-    delete cm;
-
-    return cllp;
-  }
-
-} // end namespace
diff --git a/stp/AST/ToSAT.cpp b/stp/AST/ToSAT.cpp
deleted file mode 100644
index 3ad21f93..00000000
--- a/stp/AST/ToSAT.cpp
+++ /dev/null
@@ -1,1386 +0,0 @@
-/********************************************************************
- * AUTHORS: Vijay Ganesh, David L. Dill
- *
- * BEGIN DATE: November, 2005
- *
- * LICENSE: Please view LICENSE file in the home dir of this Program
- ********************************************************************/
-// -*- c++ -*-
-#include "AST.h"
-#include "ASTUtil.h"
-#include "../simplifier/bvsolver.h"
-#include <math.h>
-
-
-namespace BEEV {
-  /* FUNCTION: lookup or create a new MINISAT literal
-   * lookup or create new MINISAT Vars from the global MAP
-   * _ASTNode_to_SATVar.
-   */
-  MINISAT::Var BeevMgr::LookupOrCreateSATVar(MINISAT::Solver& newS, const ASTNode& n) {  
-    ASTtoSATMap::iterator it;  
-    MINISAT::Var v;
-    
-    //look for the symbol in the global map from ASTNodes to ints. if
-    //not found, create a S.newVar(), else use the existing one.
-    if((it = _ASTNode_to_SATVar.find(n)) == _ASTNode_to_SATVar.end()) {
-      v = newS.newVar();
-      _ASTNode_to_SATVar[n] = v;	
-      
-      //ASSUMPTION: I am assuming that the newS.newVar() call increments v
-      //by 1 each time it is called, and the initial value of a
-      //MINISAT::Var is 0.
-      _SATVar_to_AST.push_back(n);
-    }
-    else
-      v = it->second;
-    return v;
-  }
-  
-  /* FUNCTION: convert ASTClauses to MINISAT clauses and solve.
-   * Accepts ASTClauses and converts them to MINISAT clauses. Then adds
-   * the newly minted MINISAT clauses to the local SAT instance, and
-   * calls solve(). If solve returns unsat, then stop and return
-   * unsat. else continue.
-   */  
-  // FIXME: Still need to deal with TRUE/FALSE in clauses!
- bool BeevMgr::toSATandSolve(MINISAT::Solver& newS, BeevMgr::ClauseList& cll)
- {
-    CountersAndStats("SAT Solver");
-
-    //iterate through the list (conjunction) of ASTclauses cll
-    BeevMgr::ClauseList::const_iterator i = cll.begin(), iend = cll.end();
-    
-    if(i == iend)
-      FatalError("toSATandSolve: Nothing to Solve",ASTUndefined);
-    
-    //turnOffSubsumption
-    newS.turnOffSubsumption();
-
-    // (*i) is an ASTVec-ptr which denotes an ASTclause
-    for(; i!=iend; i++) {    
-      //Clause for the SATSolver
-      MINISAT::vec<MINISAT::Lit> satSolverClause;
-      
-      //now iterate through the internals of the ASTclause itself
-      ASTVec::const_iterator j = (*i)->begin(), jend = (*i)->end();
-      //j is a disjunct in the ASTclause (*i)
-      for(;j!=jend;j++) {
-
-	bool negate = (NOT == j->GetKind()) ? true : false;		
-	ASTNode n = negate ? (*j)[0] : *j;
-	
-	//Lookup or create the MINISAT::Var corresponding to the Booelan
-	//ASTNode Variable, and push into sat Solver clause
-	MINISAT::Var v = LookupOrCreateSATVar(newS,n);
-	MINISAT::Lit l(v, negate);
-	satSolverClause.push(l);
-      }
-      newS.addClause(satSolverClause);
-      // clause printing.
-      // (printClause<MINISAT::vec<MINISAT::Lit> >)(satSolverClause);
-      // cout << " 0 ";
-      // cout << endl;
-      
-      if(newS.okay()) {
-	continue;
-      }
-      else {
-	PrintStats(newS.stats);
-	return false;
-      }
-      
-      if(!newS.simplifyDB(false)) {
-      	PrintStats(newS.stats);
-      	return false;
-      }
-    }
-
-    // if input is UNSAT return false, else return true    
-    if(!newS.simplifyDB(false)) {
-      PrintStats(newS.stats);
-      return false;
-    }
-    
-    //PrintActivityLevels_Of_SATVars("Before SAT:",newS);
-    //ChangeActivityLevels_Of_SATVars(newS);
-    //PrintActivityLevels_Of_SATVars("Before SAT and after initial bias:",newS); 
-    newS.solve();
-    //PrintActivityLevels_Of_SATVars("After SAT",newS);
-
-    PrintStats(newS.stats);
-    if (newS.okay())
-      return true;
-    else
-      return false;
-  }
-
-  // GLOBAL FUNCTION: Prints statistics from the MINISAT Solver   
-  void BeevMgr::PrintStats(MINISAT::SolverStats& s) {
-    if(!stats)
-      return;
-    double  cpu_time = MINISAT::cpuTime();
-    MINISAT::int64   mem_used = MINISAT::memUsed();
-    printf("restarts              : %"I64_fmt"\n", s.starts);
-    printf("conflicts             : %-12"I64_fmt"   (%.0f /sec)\n", s.conflicts   , s.conflicts   /cpu_time);
-    printf("decisions             : %-12"I64_fmt"   (%.0f /sec)\n", s.decisions   , s.decisions   /cpu_time);
-    printf("propagations          : %-12"I64_fmt"   (%.0f /sec)\n", s.propagations, s.propagations/cpu_time);
-    printf("conflict literals     : %-12"I64_fmt"   (%4.2f %% deleted)\n", 
-           s.tot_literals, 
-           (s.max_literals - s.tot_literals)*100 / (double)s.max_literals);
-    if (mem_used != 0) printf("Memory used           : %.2f MB\n", mem_used / 1048576.0);
-    printf("CPU time              : %g s\n", cpu_time);
-    fflush(stdout);
-  }
-  
-  // Prints Satisfying assignment directly, for debugging.
-  void BeevMgr::PrintSATModel(MINISAT::Solver& newS) {
-    if(!newS.okay())
-      FatalError("PrintSATModel: NO COUNTEREXAMPLE TO PRINT",ASTUndefined);
-    // FIXME: Don't put tests like this in the print functions.  The print functions
-    // should print unconditionally.  Put a conditional around the call if you don't 
-    // want them to print
-    if(!(stats && print_nodes))
-      return;
-
-    int num_vars = newS.nVars();
-    cout << "Satisfying assignment: " << endl;
-    for (int i = 0; i < num_vars; i++) {
-      if (newS.model[i] == MINISAT::l_True) {
-	ASTNode s = _SATVar_to_AST[i];
-	cout << s << endl;
-      }
-      else if (newS.model[i] == MINISAT::l_False) {
-	ASTNode s = _SATVar_to_AST[i];
-	cout << CreateNode(NOT, s) << endl;
-      }
-    }
-  }
-
-
-  // Looks up truth value of ASTNode SYMBOL in MINISAT satisfying assignment.
-  // Returns ASTTrue if true, ASTFalse if false or undefined.
-  ASTNode BeevMgr::SymbolTruthValue(MINISAT::Solver &newS, ASTNode form) 
-  {
-    MINISAT::Var satvar = _ASTNode_to_SATVar[form];
-    if (newS.model[satvar] == MINISAT::l_True) {
-      return ASTTrue;
-    }
-    else if (newS.model[satvar] == MINISAT::l_False){
-      // False
-      return ASTFalse;
-    }
-    else {
-      return (rand() > 4096) ? ASTTrue : ASTFalse; 
-    }
-  }
-
-
-  // This function is for debugging problems with BitBlast and especially
-  // ToCNF. It evaluates the bit-blasted formula in the satisfying
-  // assignment.  While doing that, it checks that every subformula has
-  // the same truth value as its representative literal, if it has one.
-  // If this condition is violated, it halts immediately (on the leftmost
-  // lowest term).
-  // Use CreateSimpForm to evaluate, even though it's expensive, so that
-  // we can use the partial truth assignment.
-  ASTNode BeevMgr::CheckBBandCNF(MINISAT::Solver& newS, ASTNode form)
-  {
-    // Clear memo table (in case newS has changed).
-    CheckBBandCNFMemo.clear();
-    // Call recursive version that does the work.
-    return CheckBBandCNF_int(newS, form);
-  }
-
-  // Recursive body CheckBBandCNF
-  // FIXME:  Modify this to just check if result is true, and print mismatch 
-  // if not.   Might have a trace flag for the other stuff.
-  ASTNode BeevMgr::CheckBBandCNF_int(MINISAT::Solver& newS, ASTNode form)
-  {
-
-    //    cout << "++++++++++++++++" << endl << "CheckBBandCNF_int form = " <<
-    //      form << endl;
-  
-    ASTNodeMap::iterator memoit = CheckBBandCNFMemo.find(form);
-    if (memoit != CheckBBandCNFMemo.end()) {
-      // found it.  Return memoized value.
-      return memoit->second;
-    }
-
-    ASTNode result;		// return value, to memoize.
-
-    Kind k = form.GetKind();
-    switch (k) {
-    case TRUE:
-    case FALSE: {
-      return form;
-      break;
-    }
-    case SYMBOL: 
-    case BVGETBIT:  {
-      // Look up the truth value
-      // ASTNode -> Sat -> Truthvalue -> ASTTrue or ASTFalse;
-      // FIXME: Could make up a fresh var in undefined case.
-
-      result = SymbolTruthValue(newS, form);
-
-      cout << "================" << endl << "Checking BB formula:" << form << endl;
-      cout << "----------------" << endl << "Result:" << result << endl;
-
-      break;
-    }
-    default: {
-      // Evaluate the children recursively.
-      ASTVec eval_children;
-      ASTVec ch = form.GetChildren();
-      ASTVec::iterator itend = ch.end();
-      for(ASTVec::iterator it = ch.begin(); it < itend; it++) {
-	eval_children.push_back(CheckBBandCNF_int(newS, *it));
-      }
-      result = CreateSimpForm(k, eval_children);
-
-      cout << "================" << endl << "Checking BB formula:" << form << endl;
-      cout << "----------------" << endl << "Result:" << result << endl;
-
-      ASTNode replit_eval;
-      // Compare with replit, if there is one.
-      ASTNodeMap::iterator replit_it = RepLitMap.find(form);
-      if (replit_it != RepLitMap.end()) {
-	ASTNode replit = RepLitMap[form];
-	// Replit is symbol or not symbol.
-	if (SYMBOL == replit.GetKind()) {
-	  replit_eval = SymbolTruthValue(newS, replit);
-	}
-	else {
-	  // It's (NOT sym).  Get value of sym and complement.
-	  replit_eval = CreateSimpNot(SymbolTruthValue(newS, replit[0]));
-	}
-
-	cout << "----------------" << endl << "Rep lit: " << replit << endl;
-	cout << "----------------" << endl << "Rep lit value: " << replit_eval << endl;
-
-	if (result != replit_eval) {
-	  // Hit the panic button.
-	  FatalError("Truth value of BitBlasted formula disagrees with representative literal in CNF.");
-	}
-      }
-      else {
-	cout << "----------------" << endl << "No rep lit" << endl;
-      }
-
-    }
-    }
-
-    return (CheckBBandCNFMemo[form] = result);
-  }
-
-  /*FUNCTION: constructs counterexample from MINISAT counterexample
-   * step1 : iterate through MINISAT counterexample and assemble the
-   * bits for each AST term. Store it in a map from ASTNode to vector
-   * of bools (bits).
-   *
-   * step2: Iterate over the map from ASTNodes->Vector-of-Bools and
-   * populate the CounterExampleMap data structure (ASTNode -> BVConst)
-   */
-  void BeevMgr::ConstructCounterExample(MINISAT::Solver& newS) {
-    //iterate over MINISAT counterexample and construct a map from AST
-    //terms to vector of bools. We need this iteration step because
-    //MINISAT might return the various bits of a term out of
-    //order. Therfore, we need to collect all the bits and assemble
-    //them properly
-    
-    if(!newS.okay())
-      return;
-    if(!construct_counterexample)
-      return;    
-
-    CopySolverMap_To_CounterExample();
-    for (int i = 0; i < newS.nVars(); i++) {
-      //Make sure that the MINISAT::Var is defined
-      if (newS.model[i] != MINISAT::l_Undef) {
-	
-	//mapping from MINISAT::Vars to ASTNodes. We do not need to
-	//print MINISAT vars or CNF vars.
-	ASTNode s = _SATVar_to_AST[i];
-	
-	//assemble the counterexample here
-	if(s.GetKind() == BVGETBIT && s[0].GetKind() == SYMBOL) {
-	  ASTNode symbol = s[0];
-	  unsigned int symbolWidth = symbol.GetValueWidth();
-	  
-	  //'v' is the map from bit-index to bit-value
-	  hash_map<unsigned,bool> * v;	
-	  if(_ASTNode_to_Bitvector.find(symbol) == _ASTNode_to_Bitvector.end())
-	    _ASTNode_to_Bitvector[symbol] = new hash_map<unsigned,bool>(symbolWidth);	
-	  
-	  //v holds the map from bit-index to bit-value
-	  v = _ASTNode_to_Bitvector[symbol];
-	  
-	  //kk is the index of BVGETBIT
-	  unsigned int kk = GetUnsignedConst(s[1]); 	
-	  
-	  //Collect the bits of 'symbol' and store in v. Store in reverse order.
-	  if(newS.model[i]==MINISAT::l_True)
-	    (*v)[(symbolWidth-1) - kk] = true;
-	  else
-	    (*v)[(symbolWidth-1) - kk] = false;
-	}
-	else {	 
-	  if(s.GetKind() == SYMBOL && s.GetType() == BOOLEAN_TYPE) {
-	    const char * zz = s.GetName();
-	    //if the variables are not cnf variables then add them to the counterexample
-	    if(0 != strncmp("cnf",zz,3) && 0 != strcmp("*TrueDummy*",zz)) {
-	      if(newS.model[i]==MINISAT::l_True)
-		CounterExampleMap[s] = ASTTrue;
-	      else
-		CounterExampleMap[s] = ASTFalse;	    
-	    }
-	  }
-	}
-      }
-    }
-
-    //iterate over the ASTNode_to_Bitvector data-struct and construct
-    //the the aggregate value of the bitvector, and populate the
-    //CounterExampleMap datastructure
-    for(ASTtoBitvectorMap::iterator it=_ASTNode_to_Bitvector.begin(),itend=_ASTNode_to_Bitvector.end();
-	it!=itend;it++) {
-      ASTNode var = it->first;      
-      //debugging
-      //cerr << var;
-      if(SYMBOL != var.GetKind())
-	FatalError("ConstructCounterExample: error while constructing counterexample: not a variable: ",var);
-
-      //construct the bitvector value
-      hash_map<unsigned,bool> * w = it->second;
-      ASTNode value = BoolVectoBVConst(w, var.GetValueWidth());      
-      //debugging
-      //cerr << value;
-
-      //populate the counterexample datastructure. add only scalars
-      //variables which were declared in the input and newly
-      //introduced variables for array reads
-      CounterExampleMap[var] = value;
-    }
-    
-    //In this loop, we compute the value of each array read, the
-    //corresponding ITE against the counterexample generated above.
-    for(ASTNodeMap::iterator it=_arrayread_ite.begin(),itend=_arrayread_ite.end();
-	it!=itend;it++){
-      //the array read
-      ASTNode arrayread = it->first;
-      ASTNode value_ite = _arrayread_ite[arrayread];
-      
-      //convert it to a constant array-read and store it in the
-      //counter-example. First convert the index into a constant. then
-      //construct the appropriate array-read and store it in the
-      //counterexample
-      ASTNode arrayread_index = TermToConstTermUsingModel(arrayread[1]);
-      ASTNode key = CreateTerm(READ,arrayread.GetValueWidth(),arrayread[0],arrayread_index);
-
-      //Get the ITE corresponding to the array-read and convert it
-      //to a constant against the model
-      ASTNode value = TermToConstTermUsingModel(value_ite);
-      //save the result in the counter_example
-      if(!CheckSubstitutionMap(key))
-	CounterExampleMap[key] = value;      
-    }
-  } //End of ConstructCounterExample
-
-  // FUNCTION: accepts a non-constant term, and returns the
-  // corresponding constant term with respect to a model. 
-  //
-  // term READ(A,i) is treated as follows:
-  //
-  //1. If (the boolean variable 'ArrayReadFlag' is true && ArrayRead
-  //1. has value in counterexample), then return the value of the
-  //1. arrayread.
-  //
-  //2. If (the boolean variable 'ArrayReadFlag' is true && ArrayRead
-  //2. doesn't have value in counterexample), then return the
-  //2. arrayread itself (normalized such that arrayread has a constant
-  //2. index)
-  //
-  //3. If (the boolean variable 'ArrayReadFlag' is false) && ArrayRead
-  //3. has a value in the counterexample then return the value of the
-  //3. arrayread.
-  //
-  //4. If (the boolean variable 'ArrayReadFlag' is false) && ArrayRead
-  //4. doesn't have a value in the counterexample then return 0 as the
-  //4. value of the arrayread.
-  ASTNode BeevMgr::TermToConstTermUsingModel(const ASTNode& t, bool ArrayReadFlag) {
-    Begin_RemoveWrites = false;
-    SimplifyWrites_InPlace_Flag = false;
-    //ASTNode term = SimplifyTerm(t);
-    ASTNode term = t;
-    Kind k = term.GetKind();
-    
-
-    //cerr << "Input to TermToConstTermUsingModel: " << term << endl;
-    if(!is_Term_kind(k)) {
-      FatalError("TermToConstTermUsingModel: The input is not a term: ",term);
-    }
-    if(k == WRITE) {
-      FatalError("TermToConstTermUsingModel: The input has wrong kind: WRITE : ",term);
-    }
-    if(k == SYMBOL && BOOLEAN_TYPE == term.GetType()) {
-      FatalError("TermToConstTermUsingModel: The input has wrong kind: Propositional variable : ",term);
-    }
-
-    ASTNodeMap::iterator it1;
-    if((it1 = CounterExampleMap.find(term)) != CounterExampleMap.end()) {
-      ASTNode val = it1->second;
-      if(BVCONST != val.GetKind()) {
-	//CounterExampleMap has two maps rolled into
-	//one. SubstitutionMap and SolverMap.
-	//
-	//recursion is fine here. There are two maps that are checked
-	//here. One is the substitutionmap. We garuntee that the value
-	//of a key in the substitutionmap is always a constant.
-	//
-	//in the SolverMap we garuntee that "term" does not occur in
-	//the value part of the map
-	if(term == val) {
-	  FatalError("TermToConstTermUsingModel: The input term is stored as-is "
-		     "in the CounterExample: Not ok: ",term);    
-	}
-	return TermToConstTermUsingModel(val,ArrayReadFlag);
-      }
-      else {
-	return val;
-      }
-    }
-
-    ASTNode output;
-    switch(k) {
-    case BVCONST:
-      output = term;
-      break;
-    case SYMBOL: {
-      if(term.GetType() == ARRAY_TYPE) {
-	return term;
-      }
-
-      //when all else fails set symbol values to some constant by
-      //default. if the variable is queried the second time then add 1
-      //to and return the new value.
-      ASTNode zero = CreateZeroConst(term.GetValueWidth());
-      output = zero;
-      break;    
-    }
-    case READ: {      
-      ASTNode arrName = term[0];
-      ASTNode index = term[1];
-      if(0 == arrName.GetIndexWidth()) {
-	FatalError("TermToConstTermUsingModel: array has 0 index width: ",arrName);
-      }
-      
-      //READ over a WRITE
-      if(WRITE == arrName.GetKind()) {
-	ASTNode wrtterm = Expand_ReadOverWrite_UsingModel(term, ArrayReadFlag);
-	if(wrtterm == term) {
-	  FatalError("TermToConstTermUsingModel: Read_Over_Write term must be expanded into an ITE", term);
-	}
-	ASTNode rtterm = TermToConstTermUsingModel(wrtterm,ArrayReadFlag);	
-	return rtterm;
-      } 
-      //READ over an ITE
-      if(ITE == arrName.GetKind()) {
-	arrName = TermToConstTermUsingModel(arrName,ArrayReadFlag);
-      }
-
-      ASTNode modelentry;
-      if(CounterExampleMap.find(index) != CounterExampleMap.end()) {	
-	//index has a const value in the CounterExampleMap
-	ASTNode indexVal = CounterExampleMap[index];
-	modelentry = CreateTerm(READ, arrName.GetValueWidth(), arrName, indexVal);
-      }
-      else { 
-	//index does not have a const value in the CounterExampleMap. compute it.
-	ASTNode indexconstval = TermToConstTermUsingModel(index,ArrayReadFlag);
-	//update model with value of the index
-	//CounterExampleMap[index] = indexconstval;
-	modelentry = CreateTerm(READ,arrName.GetValueWidth(), arrName,indexconstval);	
-      }
-      //modelentry is now an arrayread over a constant index
-      BVTypeCheck(modelentry);
-      
-      //if a value exists in the CounterExampleMap then return it
-      if(CounterExampleMap.find(modelentry) != CounterExampleMap.end()) {
-	output = TermToConstTermUsingModel(CounterExampleMap[modelentry],ArrayReadFlag);
-      }
-      else if(ArrayReadFlag) {
-	//return the array read over a constantindex
-	output = modelentry;
-      }
-      else {
-	//when all else fails set symbol values to some constant by
-	//default. if the variable is queried the second time then add 1
-	//to and return the new value.
-	ASTNode zero = CreateZeroConst(modelentry.GetValueWidth());
-	output = zero;
-      }
-      break;
-    }
-    case ITE: {
-      ASTNode condcompute = ComputeFormulaUsingModel(term[0]);
-      if(ASTTrue == condcompute) {
-	output = TermToConstTermUsingModel(term[1],ArrayReadFlag);
-      }
-      else if(ASTFalse == condcompute) {
-	output = TermToConstTermUsingModel(term[2],ArrayReadFlag);
-      } 
-      else {
-	cerr << "TermToConstTermUsingModel: termITE: value of conditional is wrong: " << condcompute << endl; 
-	FatalError(" TermToConstTermUsingModel: termITE: cannot compute ITE conditional against model: ",term);
-      }
-      break;
-    }
-    default: {
-      ASTVec c = term.GetChildren();
-      ASTVec o;
-      for(ASTVec::iterator it=c.begin(),itend=c.end();it!=itend;it++) {
-	ASTNode ff = TermToConstTermUsingModel(*it,ArrayReadFlag);
-	o.push_back(ff);
-      }
-      output = CreateTerm(k,term.GetValueWidth(),o);
-      //output is a CONST expression. compute its value and store it
-      //in the CounterExampleMap
-      ASTNode oo = BVConstEvaluator(output);
-      //the return value
-      output = oo;
-      break;
-    }
-    }
-
-    //when this flag is false, we should compute the arrayread to a
-    //constant. this constant is stored in the counter_example
-    //datastructure
-    if(!ArrayReadFlag) {
-      CounterExampleMap[term] = output;
-    }
-    
-    //cerr << "Output to TermToConstTermUsingModel: " << output << endl;
-    return output;
-  } //End of TermToConstTermUsingModel
-
-  //Expands read-over-write by evaluating (readIndex=writeIndex) for
-  //every writeindex until, either it evaluates to TRUE or all
-  //(readIndex=writeIndex) evaluate to FALSE
-  ASTNode BeevMgr::Expand_ReadOverWrite_UsingModel(const ASTNode& term, bool arrayread_flag) {
-    if(READ != term.GetKind() && 
-       WRITE != term[0].GetKind()) {
-      FatalError("RemovesWrites: Input must be a READ over a WRITE",term);
-    }
-
-    ASTNode output;
-    ASTNodeMap::iterator it1;    
-    if((it1 = CounterExampleMap.find(term)) != CounterExampleMap.end()) {
-      ASTNode val = it1->second;
-      if(BVCONST != val.GetKind()) {
-	//recursion is fine here. There are two maps that are checked
-	//here. One is the substitutionmap. We garuntee that the value
-	//of a key in the substitutionmap is always a constant.
-	if(term == val) {
-	  FatalError("TermToConstTermUsingModel: The input term is stored as-is "
-		     "in the CounterExample: Not ok: ",term);    
-	}
-	return TermToConstTermUsingModel(val,arrayread_flag);
-      }
-      else {
-	return val;
-      }
-    }
-
-    unsigned int width = term.GetValueWidth();
-    ASTNode writeA = ASTTrue; 
-    ASTNode newRead = term;
-    ASTNode readIndex = TermToConstTermUsingModel(newRead[1],false);
-    //iteratively expand read-over-write, and evaluate against the
-    //model at every iteration
-    do {
-      ASTNode write = newRead[0];
-      writeA = write[0];
-      ASTNode writeIndex = TermToConstTermUsingModel(write[1],false);
-      ASTNode writeVal = TermToConstTermUsingModel(write[2],false);
-      
-      ASTNode cond = ComputeFormulaUsingModel(CreateSimplifiedEQ(writeIndex,readIndex));
-      if(ASTTrue == cond) {
-	//found the write-value. return it
-	output = writeVal;
-	CounterExampleMap[term] = output;
-	return output;
-      }
-
-      newRead = CreateTerm(READ,width,writeA,readIndex);
-    } while(READ == newRead.GetKind() && WRITE == newRead[0].GetKind());
-    
-    output = TermToConstTermUsingModel(newRead,arrayread_flag);
-        
-    //memoize
-    CounterExampleMap[term] = output;
-    return output;  
-  } //Exand_ReadOverWrite_To_ITE_UsingModel()
-
-  /* FUNCTION: accepts a non-constant formula, and checks if the
-   * formula is ASTTrue or ASTFalse w.r.t to a model
-   */
-  ASTNode BeevMgr::ComputeFormulaUsingModel(const ASTNode& form) {
-    ASTNode in = form;
-    Kind k = form.GetKind();
-    if(!(is_Form_kind(k) && BOOLEAN_TYPE == form.GetType())) {
-      FatalError(" ComputeConstFormUsingModel: The input is a non-formula: ", form);
-    }
-
-    //cerr << "Input to ComputeFormulaUsingModel:" << form << endl;
-    ASTNodeMap::iterator it1;
-    if((it1 = ComputeFormulaMap.find(form)) != ComputeFormulaMap.end()) {
-      ASTNode res = it1->second;
-      if(ASTTrue == res || ASTFalse == res) {
-	return res;
-      }
-      else {
-	FatalError("ComputeFormulaUsingModel: The value of a formula must be TRUE or FALSE:", form);
-      }
-    }
-    
-    ASTNode t0,t1;
-    ASTNode output = ASTFalse;
-    switch(k) {
-    case TRUE:
-    case FALSE:
-      output = form;      
-      break;
-    case SYMBOL:
-      if(BOOLEAN_TYPE != form.GetType())
-	FatalError(" ComputeFormulaUsingModel: Non-Boolean variables are not formulas",form);
-      if(CounterExampleMap.find(form) != CounterExampleMap.end()) {
-	ASTNode counterexample_val = CounterExampleMap[form];
-	if(!VarSeenInTerm(form,counterexample_val)) {
-	  output = ComputeFormulaUsingModel(counterexample_val);
-	}
-	else {
-	  output = counterexample_val;
-	}
-      }
-      else
-	output = ASTFalse;
-      break;  
-    case EQ:
-    case NEQ:
-    case BVLT:
-    case BVLE:
-    case BVGT:
-    case BVGE:
-    case BVSLT:
-    case BVSLE:
-    case BVSGT:
-    case BVSGE:
-      //convert form[0] into a constant term
-      t0 = TermToConstTermUsingModel(form[0],false);
-      //convert form[0] into a constant term
-      t1 = TermToConstTermUsingModel(form[1],false);
-      output = BVConstEvaluator(CreateNode(k,t0,t1));
-      
-      //evaluate formula to false if bvdiv execption occurs while
-      //counterexample is being checked during refinement.
-      if(bvdiv_exception_occured && 
-	 counterexample_checking_during_refinement) {
-	output = ASTFalse;
-      }
-      break;   
-    case NAND: {
-      ASTNode o = ASTTrue;
-      for(ASTVec::const_iterator it=form.begin(),itend=form.end();it!=itend;it++)
-	if(ASTFalse == ComputeFormulaUsingModel(*it)) {
-	  o = ASTFalse;
-	  break;
-	}      
-      if(o == ASTTrue) 
-	output = ASTFalse;
-      else 
-	output = ASTTrue;
-      break;
-    }
-    case NOR: {
-      ASTNode o = ASTFalse;
-      for(ASTVec::const_iterator it=form.begin(),itend=form.end();it!=itend;it++)
-	if(ASTTrue == ComputeFormulaUsingModel(*it)) {
-	  o = ASTTrue;
-	  break;
-	}
-      if(o == ASTTrue) 
-	output = ASTFalse;
-      else 
-	output = ASTTrue;
-      break;
-    }
-    case NOT:
-      if(ASTTrue == ComputeFormulaUsingModel(form[0]))
-	output = ASTFalse;
-      else
-	output = ASTTrue;
-      break;
-    case OR:
-      for(ASTVec::const_iterator it=form.begin(),itend=form.end();it!=itend;it++) 
-	if(ASTTrue == ComputeFormulaUsingModel(*it))
-	  output = ASTTrue;
-      break;
-    case AND:
-      output = ASTTrue;
-      for(ASTVec::const_iterator it=form.begin(),itend=form.end();it!=itend;it++) {
-	if(ASTFalse == ComputeFormulaUsingModel(*it)) {	    
-	  output = ASTFalse;
-	  break;	  
-	}
-      }
-      break;
-    case XOR:
-      t0 = ComputeFormulaUsingModel(form[0]);
-      t1 = ComputeFormulaUsingModel(form[1]);
-      if((ASTTrue == t0 && ASTTrue == t1) || (ASTFalse == t0 && ASTFalse == t1))
-	output = ASTFalse;
-      else
-	output = ASTTrue;
-      break;
-    case IFF:
-      t0 = ComputeFormulaUsingModel(form[0]);
-      t1 = ComputeFormulaUsingModel(form[1]);
-      if((ASTTrue == t0 && ASTTrue == t1) || (ASTFalse == t0 && ASTFalse == t1))
-	output = ASTTrue;
-      else
-	output = ASTFalse;
-      break;
-    case IMPLIES:
-      t0 = ComputeFormulaUsingModel(form[0]);
-      t1 = ComputeFormulaUsingModel(form[1]);
-      if((ASTFalse == t0) || (ASTTrue == t0 && ASTTrue == t1))
-	output = ASTTrue;
-      else
-	output = ASTFalse;
-      break;    
-    case ITE:
-      t0 = ComputeFormulaUsingModel(form[0]);
-      if(ASTTrue == t0)
-	output = ComputeFormulaUsingModel(form[1]);
-      else if(ASTFalse == t0)
-	output = ComputeFormulaUsingModel(form[2]);
-      else 
-	FatalError("ComputeFormulaUsingModel: ITE: something is wrong with the formula: ",form);
-      break;
-    default:
-      FatalError(" ComputeFormulaUsingModel: the kind has not been implemented", ASTUndefined);
-      break;
-    }
-
-    //cout << "ComputeFormulaUsingModel output is:" << output << endl;
-    ComputeFormulaMap[form] = output;
-    return output;
-  }
-
-  void BeevMgr::CheckCounterExample(bool t) {
-    // FIXME:  Code is more useful if enable flags are check OUTSIDE the method.
-    // If I want to check a counterexample somewhere, I don't want to have to set
-    // the flag in order to make it actualy happen!
-
-    if(!check_counterexample) {
-      return;
-    }
-
-    //input is valid, no counterexample to check
-    if(ValidFlag)
-      return;
-
-    //t is true if SAT solver generated a counterexample, else it is false
-    if(!t)
-      FatalError("CheckCounterExample: No CounterExample to check", ASTUndefined);
-    const ASTVec c = GetAsserts();    
-    for(ASTVec::const_iterator it=c.begin(),itend=c.end();it!=itend;it++)
-      if(ASTFalse == ComputeFormulaUsingModel(*it))
-	FatalError("CheckCounterExample:counterexample bogus:"\
-		   "assert evaluates to FALSE under counterexample: NOT OK",*it);
-        
-    if(ASTTrue == ComputeFormulaUsingModel(_current_query))
-      FatalError("CheckCounterExample:counterexample bogus:"\
-		 "query evaluates to TRUE under counterexample: NOT OK",_current_query);
-  }
-
-  /* FUNCTION: prints a counterexample for INVALID inputs.  iterate
-   * through the CounterExampleMap data structure and print it to
-   * stdout
-   */
-  void BeevMgr::PrintCounterExample(bool t, std::ostream& os) {
-    //global command-line option
-    // FIXME: This should always print the counterexample.  If you want
-    // to turn it off, check the switch at the point of call.
-    if(!print_counterexample)
-      return;
-
-    //input is valid, no counterexample to print
-    if(ValidFlag)
-      return;
-
-    //if this option is true then print the way dawson wants using a
-    //different printer. do not use this printer.
-    if(print_arrayval_declaredorder)
-      return;
-
-    //t is true if SAT solver generated a counterexample, else it is
-    //false
-    if(!t) {
-      cerr << "PrintCounterExample: No CounterExample to print: " << endl;
-      return;
-    }
-
-    //os << "\nCOUNTEREXAMPLE: \n" << endl;
-    ASTNodeMap::iterator it  = CounterExampleMap.begin();
-    ASTNodeMap::iterator itend = CounterExampleMap.end();
-    for(;it!=itend;it++) {
-      ASTNode f = it->first;
-      ASTNode se = it->second;
-      
-      if(ARRAY_TYPE == se.GetType()) {
-	FatalError("TermToConstTermUsingModel: entry in counterexample is an arraytype. bogus:",se);
-      }
-
-      //skip over introduced variables
-      if(f.GetKind() == SYMBOL && (_introduced_symbols.find(f) != _introduced_symbols.end())) 
-	continue;
-      if(f.GetKind() == SYMBOL || 
-	 (f.GetKind() == READ && f[0].GetKind() == SYMBOL && f[1].GetKind() == BVCONST)) {
-	os << "ASSERT( ";
-	f.PL_Print(os,0);
-	os << " = ";	
-	if(BITVECTOR_TYPE == se.GetType()) {
-	  TermToConstTermUsingModel(se,false).PL_Print(os,0);
-	}
-	else {
-	  se.PL_Print(os,0);
-	}
-	os << " );" << endl;
-      }
-    }	      
-    //os << "\nEND OF COUNTEREXAMPLE" << endl;
-  } //End of PrintCounterExample
-
-  /* iterate through the CounterExampleMap data structure and print it
-   * to stdout. this function prints only the declared array variables
-   * IN the ORDER in which they were declared. It also assumes that
-   * the variables are of the form 'varname_number'. otherwise it will
-   * not print anything. This function was specifically written for
-   * Dawson Engler's group (bug finding research group at Stanford)
-   */
-  void BeevMgr::PrintCounterExample_InOrder(bool t) {
-    //global command-line option to print counterexample. we do not
-    //want both counterexample printers to print at the sametime.
-    // FIXME: This should always print the counterexample.  If you want
-    // to turn it off, check the switch at the point of call.
-    if(print_counterexample)
-      return;
-
-    //input is valid, no counterexample to print
-    if(ValidFlag)
-      return;
-    
-    //print if the commandline option is '-q'. allows printing the
-    //counterexample in order.
-    if(!print_arrayval_declaredorder)
-      return;
-
-    //t is true if SAT solver generated a counterexample, else it is
-    //false
-    if(!t) {
-      cerr << "PrintCounterExample: No CounterExample to print: " << endl;
-      return;
-    }
-    
-    //vector to store the integer values
-    std::vector<int> out_int;	
-    cout << "% ";
-    for(ASTVec::iterator it=_special_print_set.begin(),itend=_special_print_set.end();
-	it!=itend;it++) {
-      if(ARRAY_TYPE == it->GetType()) {
-	//get the name of the variable
-	const char * c = it->GetName();
-	std::string ss(c);
-	if(!(0 == strncmp(ss.c_str(),"ini_",4)))
-	  continue;
-	reverse(ss.begin(),ss.end());
-
-	//cout << "debugging: " << ss;
-	size_t pos = ss.find('_',0);
-	if(!(0 < pos && pos < ss.size()))
-	  continue;
-
-	//get the associated length
-	std::string sss = ss.substr(0,pos);
-	reverse(sss.begin(),sss.end());
-	int n = atoi(sss.c_str());
-
-	it->PL_Print(cout,2);
-	for(int j=0;j < n; j++) {
-	  ASTNode index = CreateBVConst(it->GetIndexWidth(),j);
-	  ASTNode readexpr = CreateTerm(READ,it->GetValueWidth(),*it,index);
-	  ASTNode val = GetCounterExample(t, readexpr);
-	  //cout << "ASSERT( ";
-	  //cout << " = ";	  
-	  out_int.push_back(GetUnsignedConst(val));
-	  //cout << "\n";
-	}
-      }
-    }
-    cout << endl;
-    for(unsigned int jj=0; jj < out_int.size();jj++)
-      cout << out_int[jj] << endl;
-    cout << endl;
-  } //End of PrintCounterExample_InOrder
-
-  /* FUNCTION: queries the CounterExampleMap object with 'expr' and
-   * returns the corresponding counterexample value.
-   */
-  ASTNode BeevMgr::GetCounterExample(bool t, const ASTNode& expr) {    
-    //input is valid, no counterexample to get
-    if(ValidFlag)
-      return ASTUndefined;
-    
-    if(BOOLEAN_TYPE == expr.GetType()) {
-      return ComputeFormulaUsingModel(expr);
-    }
-
-    if(BVCONST == expr.GetKind()) {
-      return expr;
-    }
-
-    ASTNodeMap::iterator it;
-    ASTNode output;
-    if((it = CounterExampleMap.find(expr)) != CounterExampleMap.end())
-      output =  TermToConstTermUsingModel(CounterExampleMap[expr],false);
-    else
-      output = CreateZeroConst(expr.GetValueWidth());
-    return output;
-  } //End of GetCounterExample
-
-  // FIXME:  Don't use numeric codes.  Use an enum type!
-  //Acceps a query, calls the SAT solver and generates Valid/InValid.
-  //if returned 0 then input is INVALID
-  //if returned 1 then input is VALID
-  //if returned 2 then ERROR
-  int BeevMgr::TopLevelSAT( const ASTNode& inputasserts, const ASTNode& query) {  
-    /******start solving**********/
-    ASTNode q = CreateNode(AND, inputasserts, CreateNode(NOT,query));
-    ASTNode orig_input = q;
-    ASTNodeStats("input asserts and query: ", q);
- 
-    ASTNode newq = q;
-    //round of substitution, solving, and simplification. ensures that
-    //DAG is minimized as much as possibly, and ideally should
-    //garuntee that all liketerms in BVPLUSes have been combined.
-    BVSolver bvsolver(this);
-    SimplifyWrites_InPlace_Flag = false;
-    Begin_RemoveWrites = false;
-    start_abstracting = false;    
-    TermsAlreadySeenMap.clear();
-    do {
-      q = newq;
-      newq = CreateSubstitutionMap(newq);
-      //ASTNodeStats("after pure substitution: ", newq);
-      newq = SimplifyFormula_TopLevel(newq,false);
-      //ASTNodeStats("after simplification: ", newq);
-      //newq = bvsolver.TopLevelBVSolve(newq);
-      //ASTNodeStats("after solving: ", newq);      
-    }while(q!=newq);
-
-    ASTNodeStats("Before SimplifyWrites_Inplace begins: ", newq);
-    SimplifyWrites_InPlace_Flag = true;
-    Begin_RemoveWrites = false;
-    start_abstracting = false;
-    TermsAlreadySeenMap.clear();
-    do {
-      q = newq;
-      //newq = CreateSubstitutionMap(newq);
-      //ASTNodeStats("after pure substitution: ", newq);
-      newq = SimplifyFormula_TopLevel(newq,false);
-      //ASTNodeStats("after simplification: ", newq);
-      newq = bvsolver.TopLevelBVSolve(newq);
-      //ASTNodeStats("after solving: ", newq);      
-    }while(q!=newq);
-    ASTNodeStats("After SimplifyWrites_Inplace: ", newq);        
-
-    start_abstracting = (arraywrite_refinement) ? true : false;
-    SimplifyWrites_InPlace_Flag = false;
-    Begin_RemoveWrites = (start_abstracting) ? false : true;    
-    if(start_abstracting) {
-      ASTNodeStats("before abstraction round begins: ", newq);
-    }
-
-    TermsAlreadySeenMap.clear();
-    do {
-      q = newq;
-      //newq = CreateSubstitutionMap(newq);
-      //Begin_RemoveWrites = true;
-      //ASTNodeStats("after pure substitution: ", newq);
-      newq = SimplifyFormula_TopLevel(newq,false);
-      //ASTNodeStats("after simplification: ", newq);
-      //newq = bvsolver.TopLevelBVSolve(newq);
-      //ASTNodeStats("after solving: ", newq);
-    }while(q!=newq);
-
-    if(start_abstracting) {
-      ASTNodeStats("After abstraction: ", newq);
-    }
-    start_abstracting = false;
-    SimplifyWrites_InPlace_Flag = false;
-    Begin_RemoveWrites = false;    
-    
-    newq = TransformFormula(newq);
-    ASTNodeStats("after transformation: ", newq);
-    TermsAlreadySeenMap.clear();
-
-    int res;    
-    //solver instantiated here
-    MINISAT::Solver newS;
-    if(arrayread_refinement) {
-      counterexample_checking_during_refinement = true;
-    }
-    
-    //call SAT and check the result
-    res = CallSAT_ResultCheck(newS,newq,orig_input);
-    if(2 != res) {
-      CountersAndStats("print_func_stats");
-      return res;
-    }
-
-    res = SATBased_ArrayReadRefinement(newS,newq,orig_input);
-    if(2 != res) {
-      CountersAndStats("print_func_stats");
-      return res;
-    }
- 
-    res = SATBased_ArrayWriteRefinement(newS,orig_input);
-    if(2 != res) {
-      CountersAndStats("print_func_stats");
-      return res;
-    }          
-
-    res = SATBased_ArrayReadRefinement(newS,newq,orig_input);
-    if(2 != res) {
-      CountersAndStats("print_func_stats");
-      return res;
-    }
-
-    FatalError("TopLevelSAT: reached the end without proper conclusion:" 
-	       "either a divide by zero in the input or a bug in STP");
-    //bogus return to make the compiler shut up
-    return 2;
-  } //End of TopLevelSAT
-
-  //go over the list of indices for each array, and generate Leibnitz
-  //axioms. Then assert these axioms into the SAT solver. Check if the
-  //addition of the new constraints has made the bogus counterexample
-  //go away. if yes, return the correct answer. if no, continue adding
-  //Leibnitz axioms systematically.
-  // FIXME:  What it really does is, for each array, loop over each index i.
-  // inside that loop, it finds all the true and false axioms with i as first
-  // index.  When it's got them all, it adds the false axioms to the formula
-  // and re-solves, and returns if the result is correct.  Otherwise, it
-  // goes on to the next index.
-  // If it gets through all the indices without a correct result (which I think
-  // is impossible, but this is pretty confusing), it then solves with all
-  // the true axioms, too.
-  // This is not the most obvious way to do it, and I don't know how it 
-  // compares with other approaches (e.g., one false axiom at a time or
-  // all the false axioms each time).
-  int BeevMgr::SATBased_ArrayReadRefinement(MINISAT::Solver& newS, 
-					    const ASTNode& q, const ASTNode& orig_input) {
-    if(!arrayread_refinement)
-      FatalError("SATBased_ArrayReadRefinement: Control should not reach here");
-
-    ASTVec FalseAxiomsVec, RemainingAxiomsVec;
-    RemainingAxiomsVec.push_back(ASTTrue);   
-    FalseAxiomsVec.push_back(ASTTrue);
-
-    //in these loops we try to construct Leibnitz axioms and add it to
-    //the solve(). We add only those axioms that are false in the
-    //current counterexample. we keep adding the axioms until there
-    //are no more axioms to add
-    //
-    //for each array, fetch its list of indices seen so far
-    for(ASTNodeToVecMap::iterator iset = _arrayname_readindices.begin(), iset_end = _arrayname_readindices.end();
-	iset!=iset_end;iset++) {
-      ASTVec listOfIndices = iset->second;
-      //loop over the list of indices for the array and create LA, and add to q
-      for(ASTVec::iterator it=listOfIndices.begin(),itend=listOfIndices.end();it!=itend;it++) {
-	if(BVCONST == it->GetKind()) {
-	  continue;
-	}	
-
-	ASTNode the_index = *it;
-	//get the arrayname
-	ASTNode ArrName = iset->first;
-	// if(SYMBOL != ArrName.GetKind())
-	// 	  FatalError("SATBased_ArrayReadRefinement: arrname is not a SYMBOL",ArrName);
-	ASTNode arr_read1 = CreateTerm(READ, ArrName.GetValueWidth(), ArrName, the_index);
-	//get the variable corresponding to the array_read1
-	ASTNode arrsym1 = _arrayread_symbol[arr_read1];
-	if(!(SYMBOL == arrsym1.GetKind() || BVCONST == arrsym1.GetKind()))
-	  FatalError("TopLevelSAT: refinementloop:term arrsym1 corresponding to READ must be a var", arrsym1);
-
-	//we have nonconst index here. create Leibnitz axiom for it
-	//w.r.t every index in listOfIndices
-	for(ASTVec::iterator it1=listOfIndices.begin(),itend1=listOfIndices.end();
-	    it1!=itend1;it1++) {
-	  ASTNode compare_index = *it1;
-	  //do not compare with yourself
-	  if(the_index == compare_index)
-	    continue;
-	  
-	  //prepare for SAT LOOP 
-	  //first construct the antecedent for the LA axiom
-	  ASTNode eqOfIndices = 
-	    (exprless(the_index,compare_index)) ? 
-	    CreateSimplifiedEQ(the_index,compare_index) : CreateSimplifiedEQ(compare_index,the_index);
-	  	  
-	  ASTNode arr_read2 = CreateTerm(READ, ArrName.GetValueWidth(), ArrName, compare_index);
-	  //get the variable corresponding to the array_read2
-	  ASTNode arrsym2 = _arrayread_symbol[arr_read2];
-	  if(!(SYMBOL == arrsym2.GetKind() || BVCONST == arrsym2.GetKind()))
-	    FatalError("TopLevelSAT: refinement loop:"
-		       "term arrsym2 corresponding to READ must be a var", arrsym2);
-	  
-	  ASTNode eqOfReads = CreateSimplifiedEQ(arrsym1,arrsym2);
-	  //construct appropriate Leibnitz axiom
-	  ASTNode LeibnitzAxiom = CreateNode(IMPLIES, eqOfIndices, eqOfReads);
-	  if(ASTFalse == ComputeFormulaUsingModel(LeibnitzAxiom))
-	    //FalseAxioms = CreateNode(AND,FalseAxioms,LeibnitzAxiom);
-	    FalseAxiomsVec.push_back(LeibnitzAxiom);
-	  else
-	    //RemainingAxioms = CreateNode(AND,RemainingAxioms,LeibnitzAxiom);
-	    RemainingAxiomsVec.push_back(LeibnitzAxiom);
-	}
-	ASTNode FalseAxioms = (FalseAxiomsVec.size()>1) ? CreateNode(AND,FalseAxiomsVec) : FalseAxiomsVec[0];
-	ASTNodeStats("adding false readaxioms to SAT: ", FalseAxioms);  
-	int res2 = CallSAT_ResultCheck(newS,FalseAxioms,orig_input);
-	if(2!=res2) {
-	  return res2;
-	}	
-      }
-    }
-    ASTNode RemainingAxioms = (RemainingAxiomsVec.size()>1) ? CreateNode(AND,RemainingAxiomsVec):RemainingAxiomsVec[0];
-    ASTNodeStats("adding remaining readaxioms to SAT: ", RemainingAxioms);  
-    return CallSAT_ResultCheck(newS,RemainingAxioms,orig_input);
-  } //end of SATBased_ArrayReadRefinement
-
-  ASTNode BeevMgr::Create_ArrayWriteAxioms(const ASTNode& term, const ASTNode& newvar) {
-    if(READ != term.GetKind() && WRITE != term[0].GetKind()) {
-      FatalError("Create_ArrayWriteAxioms: Input must be a READ over a WRITE",term);
-    }
-    
-    ASTNode lhs = newvar;
-    ASTNode rhs = term;
-    ASTNode arraywrite_axiom = CreateSimplifiedEQ(lhs,rhs);
-    return arraywrite_axiom;
-  }//end of Create_ArrayWriteAxioms()
-
-  int BeevMgr::SATBased_ArrayWriteRefinement(MINISAT::Solver& newS, const ASTNode& orig_input) {
-    ASTNode writeAxiom;
-    ASTNodeMap::iterator it = ReadOverWrite_NewName_Map.begin();
-    ASTNodeMap::iterator itend = ReadOverWrite_NewName_Map.end();
-    //int count = 0;
-    //int num_write_axioms = ReadOverWrite_NewName_Map.size();
-
-    ASTVec FalseAxioms, RemainingAxioms;
-    FalseAxioms.push_back(ASTTrue);
-    RemainingAxioms.push_back(ASTTrue);
-    for(;it!=itend;it++) {
-      //Guided refinement starts here
-      ComputeFormulaMap.clear();      
-      writeAxiom = Create_ArrayWriteAxioms(it->first,it->second);
-      if(ASTFalse == ComputeFormulaUsingModel(writeAxiom)) {
-	writeAxiom = TransformFormula(writeAxiom);
-	FalseAxioms.push_back(writeAxiom);
-      }
-      else {
-	writeAxiom = TransformFormula(writeAxiom);
-	RemainingAxioms.push_back(writeAxiom);
-      }
-    }
-      
-    writeAxiom = (FalseAxioms.size() != 1) ? CreateNode(AND,FalseAxioms) : FalseAxioms[0];
-    ASTNodeStats("adding false writeaxiom to SAT: ", writeAxiom);
-    int res2 = CallSAT_ResultCheck(newS,writeAxiom,orig_input);
-    if(2!=res2) {
-      return res2;
-    }
-    
-    writeAxiom = (RemainingAxioms.size() != 1) ? CreateNode(AND,RemainingAxioms) : RemainingAxioms[0];
-    ASTNodeStats("adding remaining writeaxiom to SAT: ", writeAxiom);
-    res2 = CallSAT_ResultCheck(newS,writeAxiom,orig_input);
-    if(2!=res2) {
-	return res2;
-    }
-    
-    return 2;
-  } //end of SATBased_ArrayWriteRefinement
-
-  //Check result after calling SAT FIXME: Document arguments in
-  //comments, and give them meaningful names.  How is anyone supposed
-  //to know what "q" is?
-  int BeevMgr::CallSAT_ResultCheck(MINISAT::Solver& newS, 
-				   const ASTNode& q, const ASTNode& orig_input) {
-    //Bitblast, CNF, call SAT now
-    ASTNode BBFormula = BBForm(q);
-    //ASTNodeStats("after bitblasting", BBFormula);    
-    ClauseList *cllp = ToCNF(BBFormula);
-    // if(stats && print_nodes) {
-    //       cout << "\nClause list" << endl;
-    //       PrintClauseList(cout, *cllp);
-    //       cerr << "\n finished printing clauselist\n";
-    //     }
-
-    bool sat = toSATandSolve(newS,*cllp);    
-    // Temporary debugging call.
-    // CheckBBandCNF(newS, BBFormula);
-
-    DeleteClauseList(cllp);
-    if(!sat) {
-      PrintOutput(true);
-      return 1;
-    }
-    else if(newS.okay()) {
-      CounterExampleMap.clear();
-      ConstructCounterExample(newS);
-      if (stats && print_nodes) {
-	PrintSATModel(newS);
-      }
-      //check if the counterexample is good or not
-      ComputeFormulaMap.clear();
-      if(counterexample_checking_during_refinement)
-	bvdiv_exception_occured = false;
-      ASTNode orig_result = ComputeFormulaUsingModel(orig_input);
-      if(!(ASTTrue == orig_result || ASTFalse == orig_result))
-      	FatalError("TopLevelSat: Original input must compute to true or false against model");
-      
-//       if(!arrayread_refinement && !(ASTTrue == orig_result)) {
-// 	print_counterexample = true;
-// 	PrintCounterExample(true);
-//       	FatalError("counterexample bogus : arrayread_refinement is switched off: " 
-//       		   "EITHER all LA axioms have not been added OR bitblaster() or ToCNF()"
-// 		   "or satsolver() or counterexamplechecker() have a bug");
-//       }
-
-      // if the counterexample is indeed a good one, then return
-      // invalid
-      if(ASTTrue == orig_result) {
-	CheckCounterExample(newS.okay());
-	PrintOutput(false);
-	PrintCounterExample(newS.okay());
-	PrintCounterExample_InOrder(newS.okay());
-	return 0;	
-      }
-      // counterexample is bogus: flag it
-      else {
-	if(stats && print_nodes) {
-	  cout << "Supposedly bogus one: \n";
-	  bool tmp = print_counterexample;
-	  print_counterexample = true;
-	  PrintCounterExample(true);
-	  print_counterexample = tmp;
-	}
-
-	return 2;
-      }
-    }
-    else {
-      PrintOutput(true);
-      return -100;
-    }
-  } //end of CALLSAT_ResultCheck
-
-
-  //FUNCTION: this function accepts a boolvector and returns a BVConst   
-  ASTNode BeevMgr::BoolVectoBVConst(hash_map<unsigned,bool> * w, unsigned int l) {    
-    unsigned len = w->size();
-    if(l < len)
-      FatalError("BoolVectorBVConst : length of bitvector does not match hash_map size:",ASTUndefined,l);
-    std::string cc;
-    for(unsigned int jj = 0; jj < l; jj++) {
-      if((*w)[jj] == true)
-	cc += '1';
-      else if((*w)[jj] == false)
-	cc += '0';
-      else 
-	cc += '0';
-    }
-    return CreateBVConst(cc.c_str(),2);
-  }
-
-  void BeevMgr::PrintActivityLevels_Of_SATVars(char * init_msg, MINISAT::Solver& newS) {
-    if(!print_sat_varorder)
-      return;
-
-    ASTtoSATMap::iterator itbegin = _ASTNode_to_SATVar.begin();   
-    ASTtoSATMap::iterator itend = _ASTNode_to_SATVar.end();
-   
-    cout << init_msg;
-    cout << ": Printing activity levels of variables\n";
-    for(ASTtoSATMap::iterator it=itbegin;it!=itend;it++){
-      cout << (it->second) << "  :  ";
-      (it->first).PL_Print(cout,0);
-      cout << "   :   ";
-      cout << newS.returnActivity(it->second) << endl;
-    }
-  }
-
-  //this function biases the activity levels of MINISAT variables.
-  void BeevMgr::ChangeActivityLevels_Of_SATVars(MINISAT::Solver& newS) {
-    if(!variable_activity_optimize)
-      return;
-
-    ASTtoSATMap::iterator itbegin = _ASTNode_to_SATVar.begin();   
-    ASTtoSATMap::iterator itend = _ASTNode_to_SATVar.end();
-   
-    unsigned int index=1;
-    double base = 2;
-    for(ASTtoSATMap::iterator it=itbegin;it!=itend;it++){
-      ASTNode n = it->first;
-
-      if(BVGETBIT == n.GetKind() || NOT == n.GetKind()) {
-      	if(BVGETBIT == n.GetKind())
-      	  index = GetUnsignedConst(n[1]);
-      	else if (NOT == n.GetKind() && BVGETBIT == n[0].GetKind())
-      	  index = GetUnsignedConst(n[0][1]);
-      	else 
-      	  index = 0;
-	double initial_activity = pow(base,(double)index);
-	newS.updateInitialActivity(it->second,initial_activity);
-      } 
-      else {
-	double initial_activity = pow(base,pow(base,(double)index));
-	newS.updateInitialActivity(it->second,initial_activity);	
-      }    
-    }
-  }
-
-  //This function prints the output of the STP solver
-  void BeevMgr::PrintOutput(bool true_iff_valid) {
-    //self-explanatory
-    if(true_iff_valid) {
-      ValidFlag = true;
-      if(print_output) {
-	if(smtlib_parser_enable)
-	  cout << "unsat\n";
-	else
-	  cout << "Valid.\n";
-      }
-    }
-    else {
-      ValidFlag = false;
-      if(print_output) {
-	if(smtlib_parser_enable)
-	  cout << "sat\n";
-	else
-	  cout << "Invalid.\n";
-      }
-    }
-  }
-} //end of namespace BEEV
diff --git a/stp/AST/Transform.cpp b/stp/AST/Transform.cpp
deleted file mode 100644
index 598b831e..00000000
--- a/stp/AST/Transform.cpp
+++ /dev/null
@@ -1,492 +0,0 @@
-/********************************************************************
- * AUTHORS: Vijay Ganesh, David L. Dill
- *
- * BEGIN DATE: November, 2005
- *
- * LICENSE: Please view LICENSE file in the home dir of this Program
- ********************************************************************/
-// -*- c++ -*-
-
-#include "AST.h"
-#include <stdlib.h>
-#include <stdio.h>
-namespace BEEV {  
-  
-  //Translates signed BVDIV/BVMOD into unsigned variety
-  ASTNode BeevMgr::TranslateSignedDivMod(const ASTNode& in) {
-    if(!(SBVMOD == in.GetKind() || SBVDIV == in.GetKind())) {
-      FatalError("TranslateSignedDivMod: input must be signed DIV/MOD\n",in);
-    }
-
-    ASTNode dividend = in[0];
-    ASTNode divisor  = in[1];      
-    unsigned len = in.GetValueWidth();
-    if(SBVMOD == in.GetKind()) {
-      //if(TopBit(dividend)==1) 
-      //
-      //then -BVMOD(-dividend,abs(divisor)) 
-      //
-      //else BVMOD(dividend,abs(divisor))
-
-      //create the condition for the dividend
-      ASTNode hi1  = CreateBVConst(32,len-1);
-      ASTNode one  = CreateOneConst(1);
-      ASTNode cond = CreateNode(EQ,one,CreateTerm(BVEXTRACT,1,dividend,hi1,hi1));
-
-      //create the condition and conditional for the divisor
-      ASTNode cond_divisor = CreateNode(EQ,one,CreateTerm(BVEXTRACT,1,divisor,hi1,hi1));
-      ASTNode pos_divisor  = CreateTerm(ITE,len,cond_divisor,CreateTerm(BVUMINUS,len,divisor),divisor);
-
-      //create the modulus term for each case
-      ASTNode modnode = CreateTerm(BVMOD,len,dividend,pos_divisor);
-      ASTNode minus_modnode = CreateTerm(BVMOD,len,CreateTerm(BVUMINUS,len,dividend),pos_divisor);
-      minus_modnode = CreateTerm(BVUMINUS,len,minus_modnode);
-
-      //put everything together, simplify, and return
-      ASTNode n = CreateTerm(ITE,len,cond,minus_modnode,modnode);
-      return SimplifyTerm_TopLevel(n);
-    }
-    
-    //now handle the BVDIV case
-    //if topBit(dividend) is 1 and topBit(divisor) is 0
-    //
-    //then output is -BVDIV(-dividend,divisor)
-    //
-    //elseif topBit(dividend) is 0 and topBit(divisor) is 1
-    //
-    //then output is -BVDIV(dividend,-divisor)
-    //
-    //elseif topBit(dividend) is 1 and topBit(divisor) is 1
-    //
-    // then output is BVDIV(-dividend,-divisor)
-    //
-    //else simply output BVDIV(dividend,divisor)
-    ASTNode hi1 = CreateBVConst(32,len-1);
-    ASTNode zero = CreateZeroConst(1);
-    ASTNode one = CreateOneConst(1);
-    ASTNode divnode = CreateTerm(BVDIV, len, dividend, divisor);
-
-    ASTNode cond1 = CreateNode(AND,
-			       CreateNode(EQ,zero,CreateTerm(BVEXTRACT,1,dividend,hi1,hi1)),
-			       CreateNode(EQ,one, CreateTerm(BVEXTRACT,1,divisor,hi1,hi1)));
-    ASTNode minus_divnode1 = CreateTerm(BVDIV,len,
-					dividend,
-					CreateTerm(BVUMINUS,len,divisor));
-    minus_divnode1 = CreateTerm(BVUMINUS,len,minus_divnode1);
-
-    ASTNode cond2 = CreateNode(AND,
-			       CreateNode(EQ,one,CreateTerm(BVEXTRACT,1,dividend,hi1,hi1)),
-			       CreateNode(EQ,zero,CreateTerm(BVEXTRACT,1,divisor,hi1,hi1)));
-    ASTNode minus_divnode2 = CreateTerm(BVDIV,len,
-					CreateTerm(BVUMINUS,len,dividend),
-					divisor);
-    minus_divnode2 = CreateTerm(BVUMINUS,len,minus_divnode2);
-
-    ASTNode cond3 = CreateNode(AND,
-			       CreateNode(EQ,one,CreateTerm(BVEXTRACT,1,dividend,hi1,hi1)),
-			       CreateNode(EQ,one,CreateTerm(BVEXTRACT,1,divisor,hi1,hi1)));
-    ASTNode minus_divnode3 = CreateTerm(BVDIV,len,
-					CreateTerm(BVUMINUS,len,dividend),
-					CreateTerm(BVUMINUS,len,divisor));
-    ASTNode n = CreateTerm(ITE,len,
-			   cond1,
-			   minus_divnode1,
-			   CreateTerm(ITE,len,
-				      cond2,
-				      minus_divnode2,
-				      CreateTerm(ITE,len,
-						 cond3,
-						 minus_divnode3,
-						 divnode)));
-  return SimplifyTerm_TopLevel(n);
-  }//end of TranslateSignedDivMod()
-
-  ASTNode BeevMgr::TransformFormula(const ASTNode& form) {
-    ASTNode result;
-
-    ASTNode simpleForm = form;
-    Kind k = simpleForm.GetKind();
-    if(!(is_Form_kind(k) && BOOLEAN_TYPE == simpleForm.GetType())) {
-      //FIXME: "You have inputted a NON-formula"?
-      FatalError("TransformFormula: You have input a NON-formula",simpleForm);
-    }
-
-    ASTNodeMap::iterator iter;
-    if((iter = TransformMap.find(simpleForm)) != TransformMap.end())
-      return iter->second;
-
-    switch(k) {
-    case TRUE:
-    case FALSE: {
-      result = simpleForm;
-      break;
-    }
-    case NOT: {
-      ASTVec c;
-      c.push_back(TransformFormula(simpleForm[0]));
-      result = CreateNode(NOT,c);      
-      break;
-    }
-    case BVLT:
-    case BVLE:
-    case BVGT:
-    case BVGE:
-    case BVSLT:
-    case BVSLE:
-    case BVSGT:
-    case BVSGE:      
-    case NEQ: {
-      ASTVec c;
-      c.push_back(TransformTerm(simpleForm[0]));      
-      c.push_back(TransformTerm(simpleForm[1]));
-      result = CreateNode(k,c);
-      break;
-    }
-    case EQ: {
-      ASTNode term1 = TransformTerm(simpleForm[0]);      
-      ASTNode term2 = TransformTerm(simpleForm[1]);
-      result = CreateSimplifiedEQ(term1,term2);     
-      break;
-    }
-    case AND:
-    case OR: 
-    case NAND:
-    case NOR:
-    case IFF:
-    case XOR:
-    case ITE:
-    case IMPLIES: {
-      ASTVec vec;
-      ASTNode o;
-      for (ASTVec::const_iterator it = simpleForm.begin(),itend=simpleForm.end(); it != itend; it++){
-	o = TransformFormula(*it);	
-	vec.push_back(o);
-      }
-
-      result = CreateNode(k, vec);
-      break;
-    }
-    default:
-      if(k == SYMBOL && BOOLEAN_TYPE == simpleForm.GetType())
-	result = simpleForm;      
-      else {
-	cerr << "The input is: " << simpleForm << endl;
-	cerr << "The valuewidth of input is : " << simpleForm.GetValueWidth() << endl;
-	FatalError("TransformFormula: Illegal kind: ",ASTUndefined, k);
-      }
-      break;    
-    } 
-    //BVTypeCheck(result);
-    TransformMap[simpleForm] = result;
-    return result;
-  } //End of TransformFormula
-
-  ASTNode BeevMgr::TransformTerm(const ASTNode& inputterm) {
-    ASTNode result;
-    ASTNode term = inputterm;
-
-    Kind k = term.GetKind();
-    if(!is_Term_kind(k))
-      FatalError("TransformTerm: Illegal kind: You have input a nonterm:", inputterm, k);
-    ASTNodeMap::iterator iter;
-    if((iter = TransformMap.find(term)) != TransformMap.end())
-      return iter->second;
-    switch(k) {
-    case SYMBOL: {
-      // ASTNodeMap::iterator itsym;
-//       if((itsym = CounterExampleMap.find(term)) != CounterExampleMap.end())	
-//       	result = itsym->second;
-//       else
-	result = term;
-      break;
-    }
-    case BVCONST:
-      result = term;
-      break;
-    case WRITE:
-      FatalError("TransformTerm: this kind is not supported",term);
-      break;
-    case READ:
-      result = TransformArray(term);
-      break;
-    case ITE: {
-      ASTNode cond = term[0];
-      ASTNode thn  = term[1];
-      ASTNode els  = term[2];
-      cond = TransformFormula(cond);
-      thn = TransformTerm(thn);
-      els = TransformTerm(els);
-      //result = CreateTerm(ITE,term.GetValueWidth(),cond,thn,els);
-      result = CreateSimplifiedTermITE(cond,thn,els);
-      result.SetIndexWidth(term.GetIndexWidth());
-      break;
-    }
-    default: {
-      ASTVec c = term.GetChildren();
-      ASTVec::iterator it = c.begin();
-      ASTVec::iterator itend = c.end();
-      unsigned width = term.GetValueWidth();
-      unsigned indexwidth = term.GetIndexWidth();
-      ASTVec o;
-      for(;it!=itend;it++) {
-	o.push_back(TransformTerm(*it));
-      }
-
-      result = CreateTerm(k,width,o);
-      result.SetIndexWidth(indexwidth);
-
-      if(SBVDIV == result.GetKind() || SBVMOD == result.GetKind()) {
-	result = TranslateSignedDivMod(result);
-      }
-      break;
-    }
-    }
-
-    TransformMap[term] = result;
-    if(term.GetValueWidth() != result.GetValueWidth())
-      FatalError("TransformTerm: result and input terms are of different length", result);
-    if(term.GetIndexWidth() != result.GetIndexWidth()) {
-      cerr << "TransformTerm: input term is : " << term << endl;
-      FatalError("TransformTerm: result and input terms have different index length", result);
-    }
-    return result;
-  } //End of TransformTerm
-
-  /* This function transforms Array Reads, Read over Writes, Read over
-   * ITEs into flattened form.
-   *
-   * Transform1: Suppose there are two array reads in the input
-   * Read(A,i) and Read(A,j) over the same array. Then Read(A,i) is
-   * replaced with a symbolic constant, say v1, and Read(A,j) is
-   * replaced with the following ITE:
-   *
-   * ITE(i=j,v1,v2)
-   *
-   * Transform2:
-   * 
-   * Transform3:
-   */
-  ASTNode BeevMgr::TransformArray(const ASTNode& term) {
-    ASTNode result = term;
-
-    unsigned int width = term.GetValueWidth();
-    Kind k = term.GetKind();
-    if (!is_Term_kind(k))
-      FatalError("TransformArray: Illegal kind: You have input a nonterm:", ASTUndefined, k);
-    ASTNodeMap::iterator iter;
-    if((iter = TransformMap.find(term)) != TransformMap.end())
-      return iter->second;
-
-    switch(k) {
-      //'term' is of the form READ(arrName, readIndex) 
-    case READ: {
-      ASTNode arrName = term[0];
-      switch (arrName.GetKind()) {
-      case SYMBOL: {
-	/* input is of the form: READ(A, readIndex)
-	 * 
-	 * output is of the from: A1, if this is the first READ over A
-         *                           
-	 *                        ITE(previous_readIndex=readIndex,A1,A2)
-	 *                        
-         *                        .....
-	 */
-
-	//  Recursively transform read index, which may also contain reads.
-	ASTNode readIndex = TransformTerm(term[1]);	
-	ASTNode processedTerm = CreateTerm(READ,width,arrName,readIndex);
-	
-	//check if the 'processedTerm' has a corresponding ITE construct
-	//already. if so, return it. else continue processing.
-	ASTNodeMap::iterator it;
-	if((it = _arrayread_ite.find(processedTerm)) != _arrayread_ite.end()) {
-	  result = it->second;	
-	  break;
-	}
-	//Constructing Symbolic variable corresponding to 'processedTerm'
-	ASTNode CurrentSymbol;
-	ASTNodeMap::iterator it1;
-	// First, check if read index is constant and it has a constant value in the substitution map.
-	if(CheckSubstitutionMap(processedTerm,CurrentSymbol)) {
-	  _arrayread_symbol[processedTerm] = CurrentSymbol;
-	}
-	// Check if it already has an abstract variable.
-	else if((it1 = _arrayread_symbol.find(processedTerm)) != _arrayread_symbol.end()) {
-	  CurrentSymbol = it1->second;
-	}
-	else {
-	  // Make up a new abstract variable.
-	  // FIXME: Make this into a method (there already may BE a method) and
-	  // get rid of the fixed-length buffer!
-	  //build symbolic name corresponding to array read. The symbolic
-	  //name has 2 components: stringname, and a count
-	  const char * b = arrName.GetName();
-	  std::string c(b);
-	  char d[32];
-	  sprintf(d,"%d",_symbol_count++);
-	  std::string ccc(d);
-	  c += "array_" + ccc;
-	  
-	  CurrentSymbol = CreateSymbol(c.c_str());
-	  CurrentSymbol.SetValueWidth(processedTerm.GetValueWidth());
-	  CurrentSymbol.SetIndexWidth(processedTerm.GetIndexWidth());
-	  _arrayread_symbol[processedTerm] = CurrentSymbol;	  
-	}
-	
-	//list of array-read indices corresponding to arrName, seen while
-	//traversing the AST tree. we need this list to construct the ITEs
-	// Dill: we hope to make this irrelevant.  Harmless for now.
-	ASTVec readIndices = _arrayname_readindices[arrName];
-	
-	//construct the ITE structure for this array-read
-	ASTNode ite = CurrentSymbol;
-	_introduced_symbols.insert(CurrentSymbol);
-	BVTypeCheck(ite);
-	
-	if(arrayread_refinement) {
-	  // ite is really a variable here; it is an ite in the
-	  // else-branch
-	  result = ite;
-	}
-	else {
-	  // Full Seshia transform if we're not doing read refinement.
-	  //do not loop if the current readIndex is a BVCONST
-	  // if(BVCONST == term[1].GetKind() && !SeenNonConstReadIndex && optimize) {
-	  // 	    result = ite; 
-	  // 	  }
-	  // 	  else {	  
-	    //else part: SET the SeenNonConstReadIndex var, and do the hard work
-	    //SeenNonConstReadIndex = true;
-	    ASTVec::reverse_iterator it2=readIndices.rbegin();
-	    ASTVec::reverse_iterator it2end=readIndices.rend();
-	    for(;it2!=it2end;it2++) {
-	      ASTNode cond = CreateSimplifiedEQ(readIndex,*it2);
-	      if(ASTFalse == cond)
-		continue;
-	      
-	      ASTNode arrRead = CreateTerm(READ,width,arrName,*it2);
-	      //Good idea to TypeCheck internally constructed nodes
-	      BVTypeCheck(arrRead);
-	      
-	      ASTNode arrayreadSymbol = _arrayread_symbol[arrRead];
-	      if(arrayreadSymbol.IsNull())
-		FatalError("TransformArray:symbolic variable for processedTerm, p," 
-			   "does not exist:p = ",arrRead);
-	      ite = CreateSimplifiedTermITE(cond,arrayreadSymbol,ite);
-	    }
-	    result = ite;
-	    //}
-	}
-	
-	_arrayname_readindices[arrName].push_back(readIndex);	
-	//save the ite corresponding to 'processedTerm'
-	_arrayread_ite[processedTerm] = result;
-	break;
-      } //end of READ over a SYMBOL
-      case WRITE:{	
-	/* The input to this case is: READ((WRITE A i val) j)
-	 *
-	 * The output of this case is: ITE( (= i j) val (READ A i))
-	 */
-	
-	/* 1. arrName or term[0] is infact a WRITE(A,i,val) expression
-	 *
-	 * 2. term[1] is the read-index j
-	 *
-	 * 3. arrName[0] is the new arrName i.e. A. A can be either a
-              SYMBOL or a nested WRITE. no other possibility
-	 *
-	 * 4. arrName[1] is the WRITE index i.e. i
-	 *
-	 * 5. arrName[2] is the WRITE value i.e. val (val can inturn
-	 *    be an array read)
-	 */
-	ASTNode readIndex = TransformTerm(term[1]);
-	ASTNode writeIndex = TransformTerm(arrName[1]);
-	ASTNode writeVal = TransformTerm(arrName[2]);
-	
-	if(!(SYMBOL == arrName[0].GetKind() || 
-	     WRITE == arrName[0].GetKind())) 
-	  FatalError("TransformArray: An array write is being attempted on a non-array:",term);
-	if(ARRAY_TYPE != arrName[0].GetType())
-	  FatalError("TransformArray: An array write is being attempted on a non-array:",term);
-	
-	ASTNode cond = CreateSimplifiedEQ(writeIndex,readIndex);
-	//TypeCheck internally created node
-	BVTypeCheck(cond);
-	ASTNode readTerm = CreateTerm(READ,width,arrName[0],readIndex);
-	//TypeCheck internally created node
-	BVTypeCheck(readTerm);
-	ASTNode readPushedIn = TransformArray(readTerm);
-	//TypeCheck internally created node
-	BVTypeCheck(readPushedIn);
-	//result = CreateTerm(ITE, arrName[0].GetValueWidth(),cond,writeVal,readPushedIn);
-	result = CreateSimplifiedTermITE(cond,writeVal,readPushedIn);
-
-	//Good idea to typecheck terms created inside the system
-	BVTypeCheck(result);
-	break;
-      } //end of READ over a WRITE
-      case ITE: {
-	/* READ((ITE cond thn els) j) 
-	 *
-	 * is transformed into
-	 *
-	 * (ITE cond (READ thn j) (READ els j))
-	 */
-	
-	//(ITE cond thn els)
-	ASTNode term0 = term[0];
-	//READINDEX j
-	ASTNode j = TransformTerm(term[1]);
-	
-	ASTNode cond = term0[0];
-	//first array 
-	ASTNode t01  = term0[1];
-	//second array
-	ASTNode t02  = term0[2];
-	
-	cond = TransformFormula(cond);
-	ASTNode thn = TransformTerm(t01);
-	ASTNode els = TransformTerm(t02);
-	
-	if(!(t01.GetValueWidth() == t02.GetValueWidth() &&
-	     t01.GetValueWidth() == thn.GetValueWidth() &&
-	     t01.GetValueWidth() == els.GetValueWidth()))
-	  FatalError("TransformArray: length of THENbranch != length of ELSEbranch in the term t = \n",term);
-
-	if(!(t01.GetIndexWidth() == t02.GetIndexWidth() &&
-	     t01.GetIndexWidth() == thn.GetIndexWidth() &&
-	     t01.GetIndexWidth() == els.GetIndexWidth()))
-	  FatalError("TransformArray: length of THENbranch != length of ELSEbranch in the term t = \n",term);
-
-	//(READ thn j)
-	ASTNode thnRead = CreateTerm(READ,width,thn,j);
-	BVTypeCheck(thnRead);
-	thnRead = TransformArray(thnRead);
-	
-	//(READ els j)
-	ASTNode elsRead = CreateTerm(READ,width,els,j);
-	BVTypeCheck(elsRead);
-	elsRead = TransformArray(elsRead);
-	
-	//(ITE cond (READ thn j) (READ els j))
-	result = CreateSimplifiedTermITE(cond,thnRead,elsRead);
-	BVTypeCheck(result);
-      break;
-      }
-      default:
-	FatalError("TransformArray: The READ is NOT over SYMBOL/WRITE/ITE",term);
-	break;
-      } 
-      break;
-    } //end of READ switch
-    default:
-      FatalError("TransformArray: input term is of wrong kind: ",ASTUndefined);
-      break;
-    }
-    
-    TransformMap[term] = result;
-    return result;
-  } //end of TransformArray()  
-} //end of namespace BEEV
diff --git a/stp/AST/genkinds.pl b/stp/AST/genkinds.pl
deleted file mode 100755
index 672481ad..00000000
--- a/stp/AST/genkinds.pl
+++ /dev/null
@@ -1,123 +0,0 @@
-#!/usr/bin/perl -w
-
-#AUTHORS: Vijay Ganesh, David L. Dill BEGIN DATE: November, 2005
-#LICENSE: Please view LICENSE file in the home dir of this Program
-#given a file containing kind names, one per line produces .h and .cpp
-#files for the kinds.
-
-#globals
-@kindnames = ();
-$minkids = 0;
-$maxkids = 0;
-@cat_bits = ();
-@category_names = ();
-%cat_index = ();
-
-$now = localtime time;
-
-sub read_kind_defs {
-    open(KFILE, "< ASTKind.kinds") || die "Cannot open .kinds file: $!\n";
-    @kindlines = <KFILE>;
-    close(KFILE)
-}
-
-# create lists of things indexed by kinds.
-sub split_fields {
-    my $kind_cat_bits;
-    # matches anything with three whitespace-delimited alphanumeric fields,
-    # followed by rest of line.  Automatically ignores lines beginning with '#' and blank lines.
-    for (@kindlines) {
-	if (/Categories:\s+(.*)/) {
-	    @category_names = split(/\s+/, $1);
-	    $i = 0;
-	    for (@category_names) {
-		$cat_index{$_} = $i++;
-		# print "cat_index{$_} = $i\n";
-	    }
-	}
-	elsif (/^(\w+)\s+(\w+)\s+(\w+|-)\s+(.*)/) {
-	    push(@kindnames, $1);
-	    push(@minkids, $2);
-	    push(@maxkids, $3);
-	    @kind_cats = split(/\s+/, $4);
-	    # build a bit vector of categories.
-	    $kind_cat_bits = 0;
-	    for (@kind_cats) {
-		$kind_cat_bits |= (1 << int($cat_index{$_}));
-	    }
-	    push(@cat_bits, $kind_cat_bits); 
-	}
-    }
-}
-
-sub gen_h_file {
-    open(HFILE, "> ASTKind.h") || die "Cannot open .h file: $!\n";
-
-    print HFILE 
-	"// -*- c++ -*-\n",
-	"#ifndef TESTKINDS_H\n",
-	"#define TESTKINDS_H\n",
-	"// Generated automatically by genkinds.pl from ASTKind.kinds $now.\n",
-	"// Do not edit\n",
-	"namespace BEEV {\n  typedef enum {\n";
-
-    for (@kindnames) {
-	print HFILE "    $_,\n";
-    }
-
-    print HFILE 
-	"} Kind;\n\n",
-	"extern unsigned char _kind_categories[];\n\n";
-
-    # For category named "cat", generate functions "bool is_cat_kind(k);"
-
-
-    for (@category_names) {
-	my $catname = $_;
-	my $kind_cat_bit = (1 << int($cat_index{$catname}));
-	print HFILE "inline bool is_", $catname, "_kind(Kind k) { return (_kind_categories[k] & $kind_cat_bit); }\n\n"
-    }
-
-    print HFILE
-	"extern const char *_kind_names[];\n\n",
-	"/** Prints symbolic name of kind */\n",
-	"inline ostream& operator<<(ostream &os, const Kind &kind) { os << _kind_names[kind]; return os; }\n",
-	"\n\n",
-	"}  // end namespace\n",
-	"\n\n#endif\n";
-
-    close(HFILE);
-}
-
-# generate the .cpp file
-
-sub gen_cpp_file {
-    open(CPPFILE, "> ASTKind.cpp") || die "Cannot open .h file: $!\n";
-
-    print CPPFILE
-	"// Generated automatically by genkinds.h from ASTKind.kinds $now.\n",
-	"// Do not edit\n",
-	"namespace BEEV {\n",
-	"const char * _kind_names[] =  {\n";
-    for (@kindnames) {
-	print CPPFILE "   \"$_\",\n";
-    }
-    print CPPFILE "};\n\n";
-
-    # category bits
-    print CPPFILE
-	"unsigned char _kind_categories[] = {\n";
-    for (@cat_bits) {
-	print CPPFILE "   $_,\n";
-    }
-    print CPPFILE 
-	"};\n",
-	"\n}  // end namespace\n";
-
-    close(CPPFILE);
-}
-
-&read_kind_defs;
-&split_fields;
-&gen_h_file;
-&gen_cpp_file;