A QF_ABV division has been added to the smt-lib. Update parser to read, update printe...

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

diff --git a/src/parser/smtlib2.y b/src/parser/smtlib2.y
index a94bd6c74859a8c1500838a7ee60517f3f323d38..8d138fd141007bb1e611110b8d417845eb7f79e9 100644 (file)
--- a/src/parser/smtlib2.y
+++ b/src/parser/smtlib2.y
@@ -226,6 +226,7 @@ cmdi:
        LPAREN_TOK LOGIC_TOK FORMID_TOK RPAREN_TOK
        {
          if (!(0 == strcmp($3->GetName(),"QF_BV") ||
+               0 == strcmp($3->GetName(),"QF_ABV") ||
                0 == strcmp($3->GetName(),"QF_AUFBV"))) {
            yyerror("Wrong input logic:");
          }

diff --git a/src/printer/SMTLIB2Printer.cpp b/src/printer/SMTLIB2Printer.cpp
index b723211ea5009f07afa46558e6bb82355a5324eb..dc15389946ef9bb9d475311824f79735ae77d90a 100644 (file)
--- a/src/printer/SMTLIB2Printer.cpp
+++ b/src/printer/SMTLIB2Printer.cpp
@@ -27,7 +27,7 @@ namespace printer
 void SMTLIB2_PrintBack(ostream &os, const ASTNode& n)
 {
        if (containsArrayOps(n))
-               os << "(set-logic QF_AUFBV)" << endl;
+               os << "(set-logic QF_ABV)" << endl;
        else
                os << "(set-logic QF_BV)"<< endl;