diff --git a/CHANGELOG b/CHANGELOG
index 9895063dc..6034ab589 100644
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -1,3 +1,7 @@
+# EBMC 6.0
+
+* SMV: removed legacy keywords EXTERN and switch
+
 # EBMC 5.9
 
 * Verilog: fix for four-valued | and &
diff --git a/regression/smv/smv/smv1.desc b/regression/smv/smv/smv1.desc
deleted file mode 100644
index ae4d345d5..000000000
--- a/regression/smv/smv/smv1.desc
+++ /dev/null
@@ -1,8 +0,0 @@
-CORE
-smv1.smv
---bdd
-^EXIT=0$
-^SIGNAL=0$
-^\[spec1\] .* PROVED$
---
-^warning: ignoring
diff --git a/regression/smv/smv/smv1.smv b/regression/smv/smv/smv1.smv
deleted file mode 100644
index 3ff9ba268..000000000
--- a/regression/smv/smv/smv1.smv
+++ /dev/null
@@ -1,8 +0,0 @@
-MODULE main
-
-VAR xy(1): boolean;
-VAR tmp: boolean;
-
-ASSIGN xy(1):=tmp;
-
-SPEC AG xy(1)=tmp;
diff --git a/src/smvlang/parser.y b/src/smvlang/parser.y
index f7745c8b5..fb8aacf42 100644
--- a/src/smvlang/parser.y
+++ b/src/smvlang/parser.y
@@ -257,8 +257,6 @@ static smv_parse_treet::modulet &new_module(YYSTYPE &location, YYSTYPE &module_n
 %token min_Token	"min"
 
 /* Not in the NuSMV manual */
-%token EXTERN_Token	"EXTERN"
-%token switch_Token	"switch"
 %token notin_Token	"notin"
 %token R_Token		"R"
 
@@ -280,12 +278,7 @@ static smv_parse_treet::modulet &new_module(YYSTYPE &location, YYSTYPE &module_n
 %token NOTEQUAL_Token "!="
 %token LTLT_Token     "<<"
 %token GTGT_Token     ">>"
-
-%token INC_Token
-%token DEC_Token
 %token BECOMES_Token  ":="
-%token ADD_Token
-%token SUB_Token
 
 %token IDENTIFIER_Token   "identifier"
 %token QIDENTIFIER_Token  "quoted identifier"
@@ -360,9 +353,6 @@ module_element:
            | ltl_specification
            | compute_specification
            | isa_declaration
-           /* not in the NuSMV manual */
-           | EXTERN_Token extern_var semi_opt
-           | EXTERN_Token
            ;
 
 var_declaration:
@@ -523,9 +513,6 @@ ltl_specification:
            }
            ;
  
-extern_var : variable_identifier EQUAL_Token STRING_Token
-           ;
-
 var_list   : var_decl
            | var_list var_decl
            ;
@@ -739,11 +726,6 @@ basic_expr : constant
              unary($$, ID_member, $1);
              stack_expr($$).set(ID_component_name, stack_expr($3).id());
            }
-           | basic_expr '(' basic_expr ')'
-           {
-             // Not in the NuSMV grammar.
-             binary($$, $1, ID_index, $3);
-           }
            | '(' formula ')'                      { $$=$2; }
            | NOT_Token basic_expr                 { init($$, ID_not); mto($$, $2); }
            | "abs" '(' basic_expr ')'             { unary($$, ID_smv_abs, $3); }
@@ -790,12 +772,6 @@ basic_expr : constant
                                                   { init($$, ID_if); mto($$, $1); mto($$, $3); mto($$, $5); }
            | case_Token cases esac_Token          { $$=$2; }
            | next_Token '(' basic_expr ')'        { init($$, ID_smv_next); mto($$, $3); }
-           /* Not in NuSMV manual */
-           | INC_Token '(' basic_expr ')'         { init($$, "inc"); mto($$, $3); }
-           | DEC_Token '(' basic_expr ')'         { init($$, "dec"); mto($$, $3); }
-           | ADD_Token '(' basic_expr ',' basic_expr ')' { j_binary($$, $3, ID_plus, $5); }
-           | SUB_Token '(' basic_expr ',' basic_expr ')' { init($$, ID_minus); mto($$, $3); mto($$, $5); }
-           | switch_Token '(' variable_identifier ')' '{' switches '}' { init($$, ID_switch); mto($$, $3); mto($$, $6); }
            /* CTL */
            | AX_Token  basic_expr                 { init($$, ID_AX);  mto($$, $2); }
            | AF_Token  basic_expr                 { init($$, ID_AF);  mto($$, $2); }
@@ -907,11 +883,6 @@ complex_identifier:
            {
              binary($$, $1, ID_index, $3);
            }
-           | complex_identifier '(' basic_expr ')'
-           {
-             // Not in the NuSMV grammar.
-             binary($$, $1, ID_index, $3);
-           }
            ;
 
 cases      :
@@ -924,16 +895,6 @@ case       : formula ':' formula ';'
            { binary($$, $1, ID_case, $3); }
            ;
 
-switches   :
-           { init($$, "switches"); }
-           | switches switch
-           { $$=$1; mto($$, $2); }
-           ;
-
-switch     : NUMBER_Token ':' basic_expr ';'
-           { init($$, ID_switch); mto($$, $1); mto($$, $3); }
-           ;
-
 %%
 
 int yysmverror(const std::string &error)
diff --git a/src/smvlang/scanner.l b/src/smvlang/scanner.l
index e3281493a..bcf9fa932 100644
--- a/src/smvlang/scanner.l
+++ b/src/smvlang/scanner.l
@@ -168,8 +168,6 @@ void newlocation(YYSTYPE &x)
 "min"		token(min_Token);
 
  /* Not in the NuSMV manual */
-"EXTERN"	token(EXTERN_Token);
-"switch"	token(switch_Token);
 "notin"		token(notin_Token);
 "R"		token(R_Token);