Bugfix. Maybe. Empty smtlib and smtlib2 format files would cause a segfault / bad...

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

diff --git a/src/parser/smtlib.y b/src/parser/smtlib.y
index d92fef518f98a87f132d4b63c9fce65379795498..d3ca6464f996ecd94cb7a36652099316b40e156e 100644 (file)
--- a/src/parser/smtlib.y
+++ b/src/parser/smtlib.y
@@ -236,8 +236,10 @@ LPAREN_TOK BENCHMARK_TOK bench_name bench_attributes RPAREN_TOK
   if($4 != NULL){
     if($4->size() > 1) 
       $$ = new ASTNode(parserInterface->nf->CreateNode(AND,*$4));
-    else
-      $$ = new ASTNode((*$4)[0]);         
+    else if($4->size() ==1)
+      $$ = new ASTNode((*$4)[0]);
+     else
+      $$ = new ASTNode(parserInterface->CreateNode(TRUE));     
     delete $4;
   }
   else {

diff --git a/src/parser/smtlib2.y b/src/parser/smtlib2.y
index 8d138fd141007bb1e611110b8d417845eb7f79e9..35b393b2e0152ef9e9d31184b06015a5f8d8cb5e 100644 (file)
--- a/src/parser/smtlib2.y
+++ b/src/parser/smtlib2.y
@@ -200,7 +200,10 @@ cmd: commands END
       querysmt2 = parserInterface->CreateNode(FALSE);
     }  
         
-      ((ASTVec*)AssertsQuery)->push_back(parserInterface->nf->CreateNode(AND,assertionsSMT2));
+       if (assertionsSMT2.size() > 0)
+       ((ASTVec*)AssertsQuery)->push_back(parserInterface->nf->CreateNode(AND,assertionsSMT2));
+       else
+       ((ASTVec*)AssertsQuery)->push_back(parserInterface->CreateNode(TRUE));
          ((ASTVec*)AssertsQuery)->push_back(querysmt2);
        parserInterface->letMgr.cleanupParserSymbolTable();
        YYACCEPT;