diff --git a/regression/smv/compute/compute1.desc b/regression/smv/compute/compute1.desc
new file mode 100644
index 00000000..30eae8a2
--- /dev/null
+++ b/regression/smv/compute/compute1.desc
@@ -0,0 +1,8 @@
+CORE
+compute1.smv
+
+^file .* line 3: No support for COMPUTE specifications .*$
+^EXIT=1$
+^SIGNAL=0$
+--
+--
diff --git a/regression/smv/compute/compute1.smv b/regression/smv/compute/compute1.smv
new file mode 100644
index 00000000..06607abe
--- /dev/null
+++ b/regression/smv/compute/compute1.smv
@@ -0,0 +1,3 @@
+MODULE main
+
+COMPUTE MIN [TRUE, TRUE];
diff --git a/regression/smv/constants/constants1.desc b/regression/smv/constants/constants1.desc
new file mode 100644
index 00000000..a7fa5e35
--- /dev/null
+++ b/regression/smv/constants/constants1.desc
@@ -0,0 +1,8 @@
+CORE
+constants1.smv
+
+^file .* line 3: No support for CONSTANTS declarations .*$
+^EXIT=1$
+^SIGNAL=0$
+--
+--
diff --git a/regression/smv/constants/constants1.smv b/regression/smv/constants/constants1.smv
new file mode 100644
index 00000000..e81428c7
--- /dev/null
+++ b/regression/smv/constants/constants1.smv
@@ -0,0 +1,3 @@
+MODULE main
+
+CONSTANTS some_constant;
diff --git a/regression/smv/frozenvar/frozenvar1.desc b/regression/smv/frozenvar/frozenvar1.desc
new file mode 100644
index 00000000..67e20192
--- /dev/null
+++ b/regression/smv/frozenvar/frozenvar1.desc
@@ -0,0 +1,8 @@
+CORE
+frozenvar1.smv
+
+^file .* line 3: No support for FROZENVAR declarations$
+^EXIT=1$
+^SIGNAL=0$
+--
+--
diff --git a/regression/smv/frozenvar/frozenvar1.smv b/regression/smv/frozenvar/frozenvar1.smv
new file mode 100644
index 00000000..542fddc5
--- /dev/null
+++ b/regression/smv/frozenvar/frozenvar1.smv
@@ -0,0 +1,3 @@
+MODULE main
+
+FROZENVAR some_var : boolean;
diff --git a/regression/smv/isa/isa1.desc b/regression/smv/isa/isa1.desc
new file mode 100644
index 00000000..9b62e2f2
--- /dev/null
+++ b/regression/smv/isa/isa1.desc
@@ -0,0 +1,8 @@
+CORE
+isa1.smv
+
+^file .* line 3: No support for ISA declarations .*$
+^EXIT=1$
+^SIGNAL=0$
+--
+--
diff --git a/regression/smv/isa/isa1.smv b/regression/smv/isa/isa1.smv
new file mode 100644
index 00000000..b29aeae5
--- /dev/null
+++ b/regression/smv/isa/isa1.smv
@@ -0,0 +1,3 @@
+MODULE main
+
+ISA some_isa
diff --git a/regression/smv/ivar/ivar1.desc b/regression/smv/ivar/ivar1.desc
new file mode 100644
index 00000000..e6cb0032
--- /dev/null
+++ b/regression/smv/ivar/ivar1.desc
@@ -0,0 +1,8 @@
+CORE
+ivar1.smv
+
+^file .* line 3: No support for IVAR declarations$
+^EXIT=1$
+^SIGNAL=0$
+--
+--
diff --git a/regression/smv/ivar/ivar1.smv b/regression/smv/ivar/ivar1.smv
new file mode 100644
index 00000000..eb9ff90a
--- /dev/null
+++ b/regression/smv/ivar/ivar1.smv
@@ -0,0 +1,3 @@
+MODULE main
+
+IVAR some_input : boolean;
diff --git a/src/smvlang/parser.y b/src/smvlang/parser.y
index b4819ba2..b3b68e9f 100644
--- a/src/smvlang/parser.y
+++ b/src/smvlang/parser.y
@@ -369,7 +369,10 @@ semi_opt   :    /* empty */
 
 module_element:
              var_declaration
+           | ivar_declaration
+           | frozenvar_declaration
            | define_declaration
+           | constants_declaration
            | assign_constraint
            | trans_constraint
            | init_constraint
@@ -377,6 +380,9 @@ module_element:
            | fairness_constraint
            | ctl_specification
            | ltl_specification
+           | compute_specification
+           | isa_declaration
+           /* not in the NuSMV manual */
            | EXTERN_Token extern_var semi_opt
            | EXTERN_Token
            ;
@@ -386,11 +392,78 @@ var_declaration:
            | VAR_Token
            ;
 
+ivar_declaration:
+             IVAR_Token simple_var_list
+           {
+             yyerror("No support for IVAR declarations");
+             YYERROR;
+           }
+           ;
+
+frozenvar_declaration:
+             FROZENVAR_Token simple_var_list
+           {
+             yyerror("No support for FROZENVAR declarations");
+             YYERROR;
+           }
+           ;
+
+simple_var_list:
+             identifier ':' simple_type_specifier ';'
+           | simple_var_list identifier ':' simple_type_specifier ';'
+
 define_declaration:
              DEFINE_Token defines
            | DEFINE_Token
            ;
 
+constants_declaration:
+             CONSTANTS_Token constants_body ';'
+           {
+             yyerror("No support for CONSTANTS declarations");
+             YYERROR;
+           }
+           ;
+
+constants_body:
+             complex_identifier
+           | constants_body ',' complex_identifier
+           ;
+
+compute_specification:
+             COMPUTE_Token compute_expr
+           {
+             yyerror("No support for COMPUTE specifications");
+             YYERROR;
+           }
+           | COMPUTE_Token compute_expr ';'
+           {
+             yyerror("No support for COMPUTE specifications");
+             YYERROR;
+           }
+           | COMPUTE_Token NAME_Token identifier ":=" compute_expr
+           {
+             yyerror("No support for COMPUTE specifications");
+             YYERROR;
+           }
+           | COMPUTE_Token NAME_Token identifier ":=" compute_expr ';'
+           {
+             yyerror("No support for COMPUTE specifications");
+             YYERROR;
+           }
+           ;
+
+compute_expr:
+           ;
+
+isa_declaration:
+             ISA_Token identifier
+           {
+             yyerror("No support for ISA declarations");
+             YYERROR;
+           }
+           ;
+
 assign_constraint:
              ASSIGN_Token assignments
            | ASSIGN_Token