From: vijay_ganesh <vijay_ganesh@e59a4935-1847-0410-ae03-e826735625c1>
Date: Mon, 7 Sep 2009 00:07:31 +0000 (+0000)
Subject: changed regression names
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=661690b12ba8d40ccc703b592702415091c1f4c5;p=francis%2Fstp.git

changed regression names

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

diff --git a/Makefile b/Makefile
index 1f769ca..1e75568 100644
--- a/Makefile
+++ b/Makefile
@@ -77,8 +77,8 @@ REGRESS_LOG = `date +%Y-%m-%d`"-regress-cvc.log"
 PROGNAME=bin/stp
 ALL_OPTIONS= -l $(REGRESS_LEVEL) $(PROGNAME) $(REGRESS_TESTS)
 
-.PHONY: regressall
-regressall:
+.PHONY: regresscvc
+regresscvc:
 	@echo "*********************************************************" \
           | tee -a $(REGRESS_LOG)
 	@echo "Starting tests at" `date` | tee -a $(REGRESS_LOG)
@@ -111,8 +111,8 @@ regressbigarray:
           | tee -a $(BIGARRAY_LOG)
 
 SMT_LOG = `date +%Y-%m-%d`"-regress-smt.log"
-.PHONY: regress_smt
-regress_smt:
+.PHONY: regresssmt
+regresssmt:
 	@echo "*********************************************************" \
           | tee -a $(SMT_LOG)
 	@echo "Starting tests at" `date` | tee -a $(SMT_LOG)
@@ -126,8 +126,8 @@ regress_smt:
           | tee -a $(SMT_LOG)
 
 CAPI_LOG = `date +%Y-%m-%d`"-regress-c-api.log"
-.PHONY: regress_c_api
-regress_c_api:
+.PHONY: regresscapi
+regresscapi:
 	@echo "*********************************************************" \
           | tee -a $(CAPI_LOG)
 	@echo "Starting tests at" `date` | tee -a $(CAPI_LOG)
diff --git a/README b/README
index b3582e2..92f132c 100644
--- a/README
+++ b/README
@@ -44,6 +44,6 @@ REGRESSIONS
 Assumes you have downloaded the testcases
 
 make regresscvc
-make regress_smt
-make regress_c_api
+make regresssmt
+make regresscapi
 make regressbigarray
\ No newline at end of file
diff --git a/scripts/Makefile.in b/scripts/Makefile.in
index 6c8beaa..1e75568 100644
--- a/scripts/Makefile.in
+++ b/scripts/Makefile.in
@@ -78,7 +78,7 @@ PROGNAME=bin/stp
 ALL_OPTIONS= -l $(REGRESS_LEVEL) $(PROGNAME) $(REGRESS_TESTS)
 
 .PHONY: regresscvc
-regressall:
+regresscvc:
 	@echo "*********************************************************" \
           | tee -a $(REGRESS_LOG)
 	@echo "Starting tests at" `date` | tee -a $(REGRESS_LOG)
@@ -111,8 +111,8 @@ regressbigarray:
           | tee -a $(BIGARRAY_LOG)
 
 SMT_LOG = `date +%Y-%m-%d`"-regress-smt.log"
-.PHONY: regress_smt
-regress_smt:
+.PHONY: regresssmt
+regresssmt:
 	@echo "*********************************************************" \
           | tee -a $(SMT_LOG)
 	@echo "Starting tests at" `date` | tee -a $(SMT_LOG)
@@ -126,8 +126,8 @@ regress_smt:
           | tee -a $(SMT_LOG)
 
 CAPI_LOG = `date +%Y-%m-%d`"-regress-c-api.log"
-.PHONY: regress_c_api
-regress_c_api:
+.PHONY: regresscapi
+regresscapi:
 	@echo "*********************************************************" \
           | tee -a $(CAPI_LOG)
 	@echo "Starting tests at" `date` | tee -a $(CAPI_LOG)
diff --git a/src/parser/CVC.y b/src/parser/CVC.y
index 42ff10b..080a4fe 100644
--- a/src/parser/CVC.y
+++ b/src/parser/CVC.y
@@ -16,6 +16,12 @@
   // compile error)
 #undef __GNUC_MINOR__
 
+#define YYLTYPE_IS_TRIVIAL 1
+#define YYMAXDEPTH 10485760
+#define YYERROR_VERBOSE 1
+#define YY_EXIT_FAILURE -1
+#define YYPARSE_PARAM AssertsQuery
+
 
   extern int cvclex(void);
   extern char* yytext;
@@ -23,14 +29,8 @@
   int yyerror(const char *s) {
     cout << "syntax error: line " << cvclineno << "\n" << s << endl;    
     FatalError("");
-    return 1;			/* Dill: don't know what it should return */
+    return YY_EXIT_FAILURE;			/* Dill: don't know what it should return */
   };
-
-#define YYLTYPE_IS_TRIVIAL 1
-#define YYMAXDEPTH 10485760
-#define YYERROR_VERBOSE 1
-#define YY_EXIT_FAILURE -1
-#define YYPARSE_PARAM AssertsQuery
 %}
 
 %union {
@@ -457,10 +457,10 @@ Formula		:     '(' Formula ')' { $$ = $2; }
 			 //
 			 //increment value (BVCONST)
 			 //
-			 //formula (it can be a nested forloop)
-			 _parser_symbol_table.insert(*$3);
+			 //formula (it can be a nested forloop)			 
 			 $3->SetIndexWidth($5.indexwidth);
 			 $3->SetValueWidth($5.valuewidth);
+			 _parser_symbol_table.insert(*$3);
 			   
 			 ASTVec vec;
 			 vec.push_back(*$3);
diff --git a/src/parser/let-funcs.cpp b/src/parser/let-funcs.cpp
index 63f5a78..4699af9 100644
--- a/src/parser/let-funcs.cpp
+++ b/src/parser/let-funcs.cpp
@@ -29,11 +29,13 @@ namespace BEEV {
     ASTNodeMap::iterator it;
     if(((it = _letid_expr_map->find(var)) != _letid_expr_map->end()) && 
        it->second != ASTUndefined) {      
-      FatalError("LetExprMgr:The LET-var v has already been defined in this LET scope: v =", var);
+      FatalError("LetExprMgr:The LET-var v has already been defined"\ 
+		 "in this LET scope: v =", var);
     }
 
     if(_parser_symbol_table.find(var) != _parser_symbol_table.end()) {
-      FatalError("LetExprMgr:This var is already declared. cannot redeclare as a letvar: v =", var);
+      FatalError("LetExprMgr:This var is already declared. "\
+		 "cannot redeclare as a letvar: v =", var);
     }
 
     (*_letid_expr_map)[var] = letExpr;