SMV: do not allow defining identifiers that are already declared

VAR x : ... followed by DEFINE x := ... must be errored.

Author: kroening

Diff for: regression/smv/define/define2.desc

@@ -0,0 +1,8 @@
+CORE
+define2.smv
+
+^file .* line 6: variable `x' already declared.*$
+^EXIT=1$
+^SIGNAL=0$
+--
+--

Diff for: regression/smv/define/define2.smv

@@ -0,0 +1,6 @@
+MODULE main
+
+VAR x : boolean;
+
+-- not allowed, x is already a variable
+DEFINE x := TRUE;

Diff for: regression/smv/define/define3.desc

@@ -0,0 +1,8 @@
+CORE
+define3.smv
+
+^file .* line 6: variable `x' already defined.*$
+^EXIT=1$
+^SIGNAL=0$
+--
+--

Diff for: regression/smv/define/define3.smv

@@ -0,0 +1,6 @@
+MODULE main
+
+DEFINE x := TRUE;
+
+-- not allowed, x is already defined
+VAR x : boolean;

Diff for: src/smvlang/parser.y

@@ -489,7 +489,8 @@ define     : assignment_var BECOMES_Token formula ';'
                break;
 
              case smv_parse_treet::mc_vart::DECLARED:
-               var.var_class=smv_parse_treet::mc_vart::DEFINED;
+               yyerror("variable `"+id2string(identifier)+"' already declared");
+               YYERROR;
                break;
 
              case smv_parse_treet::mc_vart::DEFINED: