Fix. If not simplifying during parsing an assertion was violated.

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

diff --git a/src/parser/smtlib2.y b/src/parser/smtlib2.y
index cd75e6074245e6f930a795bcc0162a28c643fdb7..463260b5e707dc0d79a6167febbb8c18cda779ac 100644 (file)
--- a/src/parser/smtlib2.y
+++ b/src/parser/smtlib2.y
@@ -196,8 +196,10 @@ cmd: commands END
       querysmt2 = parserInterface->CreateNode(FALSE);
     }  
         
-       if (assertionsSMT2.size() > 0)
+       if (assertionsSMT2.size() > 1)
        ((ASTVec*)AssertsQuery)->push_back(parserInterface->nf->CreateNode(AND,assertionsSMT2));
+       else if (assertionsSMT2.size() > 0)
+       ((ASTVec*)AssertsQuery)->push_back((assertionsSMT2[0]));
        else
        ((ASTVec*)AssertsQuery)->push_back(parserInterface->CreateNode(TRUE));
          ((ASTVec*)AssertsQuery)->push_back(querysmt2);