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 0d318e8c45109c9886f13c0b74d69b5791c48600..25e5555fb8ecae7dbe19356f36a95984c7e24767 100644 (file)
--- 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 8d3b3fd36c4ae4b63090e499205a741381d51351..b723211ea5009f07afa46558e6bb82355a5324eb 100644 (file)
--- 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 8681b35feabc8ec81bcd2fda312912c4ab015843..18ccb2734dd72245a390e5bf99c8d7f2fcc295bf 100644 (file)
--- 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)
          {