From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Fri, 25 Jun 2010 05:19:52 +0000 (+0000)
Subject: Use the new method to determine whether the sub-graph contains arrays.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=310e6a3e7fbba4f749271cccc9d97305aa0a4ac3;p=francis%2Fstp.git

Use the new method to determine whether the sub-graph contains arrays.



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

diff --git a/src/printer/SMTLIB1Printer.cpp b/src/printer/SMTLIB1Printer.cpp
index 0d318e8..25e5555 100644
--- a/src/printer/SMTLIB1Printer.cpp
+++ b/src/printer/SMTLIB1Printer.cpp
@@ -32,7 +32,7 @@ namespace printer
 {
     os << "(" << endl;
     os << "benchmark blah" << endl;
-	if (containsAnyArrayOps(n))
+	if (containsArrayOps(n))
 	    os << ":logic QF_AUFBV" << endl;
 	else
 		os << ":logic QF_BV" << endl;
diff --git a/src/printer/SMTLIB2Printer.cpp b/src/printer/SMTLIB2Printer.cpp
index 8d3b3fd..b723211 100644
--- a/src/printer/SMTLIB2Printer.cpp
+++ b/src/printer/SMTLIB2Printer.cpp
@@ -26,7 +26,7 @@ namespace printer
 
 void SMTLIB2_PrintBack(ostream &os, const ASTNode& n)
 {
-	if (containsAnyArrayOps(n))
+	if (containsArrayOps(n))
 		os << "(set-logic QF_AUFBV)" << endl;
 	else
 		os << "(set-logic QF_BV)"<< endl;
diff --git a/src/printer/SMTLIBPrinter.cpp b/src/printer/SMTLIBPrinter.cpp
index 8681b35..18ccb27 100644
--- a/src/printer/SMTLIBPrinter.cpp
+++ b/src/printer/SMTLIBPrinter.cpp
@@ -27,11 +27,6 @@ static string tolower(const char * name)
 	//correctly print shared subterms inside the LET itself
 	BEEV::ASTNodeMap NodeLetVarMap1;
 
-	bool containsAnyArrayOps(const ASTNode& n)
-	{
-		return true;
-	}
-
 	  // copied from Presentation Langauge printer.
 	  ostream& SMTLIB_Print(ostream &os, const ASTNode n, const int indentation, void (*SMTLIB1_Print1)(ostream&, const ASTNode , int , bool ), bool smtlib1)
 	  {