From d496e4a417a6a8b228472e32dbe05a9114c00e3d Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 19 Jan 2011 01:05:12 +0000
Subject: [PATCH] Bugfix. Maybe. Empty smtlib and smtlib2 format files would
 cause a segfault / bad thing. I suspect these should be allowed, but haven't
 checked versus the specification.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1073 e59a4935-1847-0410-ae03-e826735625c1
---
 src/parser/smtlib.y  | 6 ++++--
 src/parser/smtlib2.y | 5 ++++-
 2 files changed, 8 insertions(+), 3 deletions(-)

diff --git a/src/parser/smtlib.y b/src/parser/smtlib.y
index d92fef5..d3ca646 100644
--- 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 8d138fd..35b393b 100644
--- 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;
-- 
2.47.3