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 1f769ca82a41657dd16417f2bd0831afd12fc151..1e7556854f23298d2a14b7a2548bc1dd99071ed1 100644 (file)
--- 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 b3582e26e461612cdf7ffe4325cfab4718b8417b..92f132cc6e1f2f8c0bc94fb1481baed6fafe20fc 100644 (file)
--- 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 6c8beaa95ae7542ed62b9dd6ec8cbc613cf88b73..1e7556854f23298d2a14b7a2548bc1dd99071ed1 100644 (file)
--- 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 42ff10b35fa23b78b4eefd35c3998950a831eff4..080a4feaf452442e0af5ac1152dad79f1a0f4b7e 100644 (file)
--- 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 63f5a780adf7e05e22e46f20e3e5c833a4dda427..4699af9c51f6eeb325170949ec57f53e8e1c527d 100644 (file)
--- 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;