From: vijay_ganesh <vijay_ganesh@e59a4935-1847-0410-ae03-e826735625c1>
Date: Thu, 12 Nov 2009 23:21:37 +0000 (+0000)
Subject: fixed a bug in the CVC parser. It was allowing the user to input only assertions... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=a650b2a53284126c0c09d2379a523c438487dffd;p=francis%2Fstp.git

fixed a bug in the CVC parser. It was allowing the user to input only assertions, and then segfaulting because there was no query.

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

diff --git a/src/main/main.cpp b/src/main/main.cpp
index 370ebd1..0e1a293 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -247,8 +247,21 @@ int main(int argc, char ** argv) {
     }
   bm->GetRunTimes()->stop(RunTimes::Parsing);
 
+  if(((ASTVec*)AssertsQuery)->empty())
+    {
+      FatalError("Input is Empty. Please enter some asserts and query\n");
+    }
+
+  if(((ASTVec*)AssertsQuery)->size() != 2)
+    {
+      FatalError("Input must contain a query\n");
+    }
+
   ASTNode asserts = (*(ASTVec*)AssertsQuery)[0];
+  //cout << "asserts: " << asserts << endl;
   ASTNode query   = (*(ASTVec*)AssertsQuery)[1];
+  //cout << "query: " << query << endl;
+
   if(bm->UserFlags.print_STPinput_back_flag)
     {
       if(bm->UserFlags.smtlib_parser_flag)
diff --git a/src/parser/CVC.y b/src/parser/CVC.y
index 6026f85..b12e3d1 100644
--- a/src/parser/CVC.y
+++ b/src/parser/CVC.y
@@ -184,7 +184,21 @@ counterexample  :      COUNTEREXAMPLE_TOK ';'
 }                              
 ;
 
-other_cmd       :      other_cmd1
+other_cmd       :
+/* other_cmd1 */
+/* { */
+/*   ASTVec aaa = ParserBM->GetAsserts(); */
+/*   if(aaa.size() == 0) */
+/*     { */
+/*       yyerror("Fatal Error: parsing:  GetAsserts() call: no assertions: "); */
+/*     } */
+
+/*   ASTNode asserts =  */
+/*     aaa.size() == 1 ?  */
+/*     aaa[0] : */
+/*     ParserBM->CreateNode(AND, aaa); */
+/*   ((ASTVec*)AssertsQuery)->push_back(asserts);   */
+/* } */
 |      Query 
 { 
   ((ASTVec*)AssertsQuery)->push_back(ParserBM->CreateNode(TRUE));
diff --git a/src/to-sat/ToCNF.cpp b/src/to-sat/ToCNF.cpp
index 36a701d..48ce34e 100644
--- a/src/to-sat/ToCNF.cpp
+++ b/src/to-sat/ToCNF.cpp
@@ -811,7 +811,7 @@ namespace BEEV
   void CNFMgr::doRenamingPosXor(const ASTNode& varphi)
   {
     CNFInfo* x = info[varphi];
-    
+
     //########################################
     // step 1, calc new variable
     //########################################
@@ -1650,6 +1650,14 @@ namespace BEEV
   {
 #ifdef FALSE
     //#ifdef CRYPTOMINISAT
+    // CNFInfo * xx = info[varphi];
+    //     if(NULL != xx
+    //        && sharesPos(*xx) > 0
+    //        && sharesNeg(*xx) > 0)
+    //       {
+    // 	return;
+    //       }
+
     ASTVec::const_iterator it = varphi.GetChildren().begin();
     ClausePtr xor_clause = new vector<const ASTNode*>();
 
diff --git a/tests/misc-tests/cryptominisat-bug.cvc b/tests/misc-tests/cryptominisat-bug.cvc
new file mode 100644
index 0000000..9bd46ed
--- /dev/null
+++ b/tests/misc-tests/cryptominisat-bug.cvc
@@ -0,0 +1,4 @@
+X : BITVECTOR(4);
+
+ASSERT 0bin0000 = BVPLUS(4,0bin0110, X);
+QUERY FALSE;
\ No newline at end of file
diff --git a/tests/misc-tests/no-query.cvc b/tests/misc-tests/no-query.cvc
new file mode 100644
index 0000000..96ef2c9
--- /dev/null
+++ b/tests/misc-tests/no-query.cvc
@@ -0,0 +1 @@
+ASSERT FALSE;
\ No newline at end of file