diff --git a/src/ebmc/smvlang/Makefile b/src/ebmc/smvlang/Makefile
new file mode 100644
index 0000000..379902a
--- /dev/null
+++ b/src/ebmc/smvlang/Makefile
@@ -0,0 +1,31 @@
+SRC = smv_language.cpp smv_parser.cpp smv_typecheck.cpp expr2smv.cpp \
+      y.tab.cpp lex.yy.cpp smv_parse_tree.cpp
+
+INCLUDES= -I .. -I ../util
+
+include ../config.inc
+include ../common
+
+CLEANFILES = smvlang$(LIBEXT) y.tab.h y.tab.cpp lex.yy.cpp y.tab.cpp.output y.output
+
+all: smvlang$(LIBEXT)
+
+###############################################################################
+
+smvlang$(LIBEXT): $(OBJ)
+	$(LINKLIB)
+
+y.tab.cpp: parser.y
+	$(YACC) $(YFLAGS) $$flags -pyysmv -d parser.y -o y.tab.cpp
+
+y.tab.h: y.tab.cpp
+	if [ -e y.tab.hpp ] ; then mv y.tab.hpp y.tab.h ; else \
+        mv y.tab.cpp.h y.tab.h ; fi
+
+lex.yy.cpp: scanner.l
+	$(LEX) -Pyysmv -olex.yy.cpp scanner.l
+
+# extra dependencies
+y.tab$(OBJEXT): y.tab.cpp y.tab.h
+lex.yy$(OBJEXT): y.tab.cpp lex.yy.cpp y.tab.h
+
diff --git a/src/ebmc/smvlang/expr2smv.cpp b/src/ebmc/smvlang/expr2smv.cpp
new file mode 100644
index 0000000..9dcb2a5
--- /dev/null
+++ b/src/ebmc/smvlang/expr2smv.cpp
@@ -0,0 +1,578 @@
+/*******************************************************************\
+
+Module:
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#include <string.h>
+
+#include <lispexpr.h>
+#include <lispirep.h>
+#include <i2string.h>
+#include <std_expr.h>
+
+#include "expr2smv.h"
+
+class expr2smvt
+{
+public:
+  bool convert_nondet_choice(const exprt &src, std::string &dest, unsigned precedence);
+
+  bool convert_binary(const exprt &src, std::string &dest, const std::string &symbol, unsigned precedence);
+
+  bool convert_unary(const exprt &src, std::string &dest, const std::string &symbol, unsigned precedence);
+
+  bool convert_index(const exprt &src, std::string &dest, unsigned precedence);
+
+  bool convert(const exprt &src, std::string &dest, unsigned &precedence);
+
+  bool convert(const exprt &src, std::string &dest);
+
+  bool convert_symbol(const exprt &src, std::string &dest, unsigned &precedence);
+
+  bool convert_next_symbol(const exprt &src, std::string &dest, unsigned &precedence);
+
+  bool convert_constant(const exprt &src, std::string &dest, unsigned &precedence);
+
+  bool convert_cond(const exprt &src, std::string &dest);
+
+  bool convert_norep(const exprt &src, std::string &dest, unsigned &precedence);
+
+  bool convert(const typet &src, std::string &dest);
+};
+
+/* SMV Operator Precedences:
+
+ 1 %left  COMMA
+ 2 %right IMPLIES
+ 3 %left  IFF
+ 4 %left  OR XOR XNOR
+ 5 %left  AND
+ 6 %left  NOT
+ 7 %left  EX AX EF AF EG AG EE AA SINCE UNTIL TRIGGERED RELEASES EBF EBG ABF ABG BUNTIL MMIN MMAX
+ 8 %left  OP_NEXT OP_GLOBAL OP_FUTURE
+ 9 %left  OP_PREC OP_NOTPRECNOT OP_HISTORICAL OP_ONCE
+10 %left  APATH EPATH
+11 %left  EQUAL NOTEQUAL LT GT LE GE
+12 %left  UNION
+13 %left  SETIN
+14 %left  MOD
+15 %left  PLUS MINUS
+16 %left  TIMES DIVIDE
+17 %left  UMINUS
+18 %left  NEXT SMALLINIT
+19 %left  DOT
+20        [ ]
+21 = max
+
+*/
+
+#define SMV_MAX_PRECEDENCE 21
+
+/*******************************************************************\
+
+Function: expr2smvt::convert_nondet_choice
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+bool expr2smvt::convert_nondet_choice(
+  const exprt &src,
+  std::string &dest,
+  unsigned precedence)
+{
+  dest="{ ";
+
+  bool first=true;
+
+  forall_operands(it, src)
+  {
+    if(first)
+      first=false;
+    else
+      dest+=", ";
+
+    std::string tmp;
+    if(convert(*it, tmp)) return true;
+    dest+=tmp;
+  }
+
+  dest+=" }";
+  return false;
+}
+
+/*******************************************************************\
+
+Function: expr2smvt::convert_cond
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+bool expr2smvt::convert_cond(
+  const exprt &src,
+  std::string &dest)
+{
+  dest="case ";
+
+  bool condition=true;
+
+  forall_operands(it, src)
+  {
+    std::string tmp;
+    if(convert(*it, tmp)) return true;
+    dest+=tmp;
+
+    if(condition)
+      dest+=": ";
+    else
+      dest+="; ";
+    
+    condition=!condition;
+  }
+
+  dest+="esac";
+  return false;
+}
+
+/*******************************************************************\
+
+Function: expr2smvt::convert_binary
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+bool expr2smvt::convert_binary(
+  const exprt &src,
+  std::string &dest,
+  const std::string &symbol,
+  unsigned precedence)
+{
+  if(src.operands().size()<2)
+    return convert_norep(src, dest, precedence);
+
+  bool first=true;
+
+  forall_operands(it, src)
+  {
+    if(first)
+      first=false;
+    else
+    {
+      dest+=' ';
+      dest+=symbol;
+      dest+=' ';
+    }
+
+    std::string op;
+    unsigned p;
+
+    if(convert(*it, op, p)) return true;
+
+    if(precedence>p) dest+='(';
+    dest+=op;
+    if(precedence>p) dest+=')';
+  }
+
+  return false;
+}
+
+/*******************************************************************\
+
+Function: expr2smvt::convert_unary
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+bool expr2smvt::convert_unary(
+  const exprt &src, std::string &dest,
+  const std::string &symbol,
+  unsigned precedence)
+{
+  if(src.operands().size()!=1)
+    return convert_norep(src, dest, precedence);
+    
+  std::string op;
+  unsigned p;
+
+  if(convert(src.op0(), op, p)) return true;
+
+  dest+=symbol;
+  if(precedence>p) dest+='(';
+  dest+=op;
+  if(precedence>p) dest+=')';
+
+  return false;
+}
+
+/*******************************************************************\
+
+Function: expr2smvt::convert_index
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+bool expr2smvt::convert_index(
+  const exprt &src,
+  std::string &dest,
+  unsigned precedence)
+{
+  if(src.operands().size()!=2)
+    return convert_norep(src, dest, precedence);
+
+  std::string op;
+  unsigned p;
+
+  if(convert(src.op0(), op, p)) return true;
+
+  if(precedence>p) dest+='(';
+  dest+=op;
+  if(precedence>p) dest+=')';
+
+  if(convert(src.op1(), op, p)) return true;
+
+  dest+='[';
+  dest+=op;
+  dest+=']';
+
+  return false;
+}
+
+/*******************************************************************\
+
+Function: expr2smvt::convert_norep
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+bool expr2smvt::convert_norep(
+  const exprt &src,
+  std::string &dest,
+  unsigned &precedence)
+{
+  precedence=SMV_MAX_PRECEDENCE;
+  dest=src.to_string();
+  return false;
+}
+
+/*******************************************************************\
+
+Function: expr2smvt::convert_symbol
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+bool expr2smvt::convert_symbol(
+  const exprt &src,
+  std::string &dest,
+  unsigned &precedence)
+{
+  precedence=SMV_MAX_PRECEDENCE;
+  dest=src.get_string(ID_identifier);
+ 
+  if(strncmp(dest.c_str(), "smv::", 5)==0)
+    dest.erase(0, 5);
+
+  return false;
+}
+
+/*******************************************************************\
+
+Function: expr2smvt::convert_next_symbol
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+bool expr2smvt::convert_next_symbol(
+  const exprt &src,
+  std::string &dest,
+  unsigned &precedence)
+{
+  std::string tmp;
+  convert_symbol(src, tmp, precedence);
+
+  dest="next("+tmp+")";
+
+  return false;
+}
+
+/*******************************************************************\
+
+Function: expr2smvt::convert_constant
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+bool expr2smvt::convert_constant(
+  const exprt &src,
+  std::string &dest,
+  unsigned &precedence)
+{
+  precedence=SMV_MAX_PRECEDENCE;
+
+  const typet &type=src.type();
+  const std::string &value=src.get_string(ID_value);
+
+  if(type.id()==ID_bool)
+  {
+    if(src.is_true())
+      dest+="TRUE";
+    else
+      dest+="FALSE";
+  }
+  else if(type.id()==ID_integer ||
+          type.id()==ID_natural ||
+          type.id()==ID_range)
+    dest=value;
+  else
+    return convert_norep(src, dest, precedence);
+
+  return false;
+}
+
+/*******************************************************************\
+
+Function: expr2smvt::convert
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+bool expr2smvt::convert(
+  const exprt &src,
+  std::string &dest,
+  unsigned &precedence)
+{
+  precedence=SMV_MAX_PRECEDENCE;
+
+  if(src.id()==ID_plus)
+    return convert_binary(src, dest, "+", precedence=15);
+
+  else if(src.id()==ID_minus)
+  {
+    if(src.operands().size()<2)
+      return convert_norep(src, dest, precedence);
+    else     
+      return convert_binary(src, dest, "-", precedence=15);
+  }
+
+  else if(src.id()==ID_unary_minus)
+  {
+    if(src.operands().size()!=1)
+      return convert_norep(src, dest, precedence);
+    else     
+      return convert_unary(src, dest, "-", precedence=17);
+  }
+
+  else if(src.id()==ID_index)
+    return convert_index(src, dest, precedence=20);
+
+  else if(src.id()==ID_mult || src.id()==ID_div)
+    return convert_binary(src, dest, src.id_string(), precedence=16);
+
+  else if(src.id()==ID_lt || src.id()==ID_gt ||
+          src.id()==ID_le || src.id()==ID_ge)
+    return convert_binary(src, dest, src.id_string(), precedence=11);
+
+  else if(src.id()==ID_equal)
+    return convert_binary(src, dest, "=", precedence=11);
+
+  else if(src.id()==ID_not)
+    return convert_unary(src, dest, "!", precedence=6);
+
+  else if(src.id()==ID_and)
+    return convert_binary(src, dest, "&", precedence=5);
+
+  else if(src.id()==ID_or)
+    return convert_binary(src, dest, "|", precedence=4);
+
+  else if(src.id()==ID_implies)
+    return convert_binary(src, dest, "->", precedence=2);
+
+  else if(src.id()=="<=>")
+    return convert_binary(src, dest, "<->", precedence=3);
+
+  else if(src.id()==ID_AG || src.id()==ID_EG ||
+          src.id()==ID_AX || src.id()==ID_EX)
+    return convert_unary(src, dest, src.id_string()+" ", precedence=7);
+
+  else if(src.id()==ID_symbol)
+    return convert_symbol(src, dest, precedence);
+
+  else if(src.id()==ID_next_symbol)
+    return convert_next_symbol(src, dest, precedence);
+
+  else if(src.id()==ID_constant)
+    return convert_constant(src, dest, precedence);
+
+  else if(src.id()=="smv_nondet_choice")
+    return convert_nondet_choice(src, dest, precedence);
+
+  else if(src.id()==ID_nondet_bool)
+  {
+    exprt nondet_choice_expr("smv_nondet_choice");
+    nondet_choice_expr.operands().clear();
+    nondet_choice_expr.operands().push_back(false_exprt());
+    nondet_choice_expr.operands().push_back(true_exprt());
+    return convert_nondet_choice(nondet_choice_expr, dest, precedence);
+  }
+
+  else if(src.id()==ID_cond)
+    return convert_cond(src, dest);
+
+  else // no SMV language expression for internal representation 
+    return convert_norep(src, dest, precedence);
+
+  return false;
+}
+
+/*******************************************************************\
+
+Function: expr2smvt::convert
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+bool expr2smvt::convert(const exprt &src, std::string &dest)
+{
+  unsigned precedence;
+  return convert(src, dest, precedence);
+}
+
+/*******************************************************************\
+
+Function: expr2smv
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+bool expr2smv(const exprt &expr, std::string &code)
+{
+  expr2smvt expr2smv;
+  return expr2smv.convert(expr, code);
+}
+
+/*******************************************************************\
+
+Function: type2smv
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+bool type2smv(const typet &type, std::string &code)
+{
+  if(type.id()==ID_bool)
+    code="boolean";
+  else if(type.id()==ID_array)
+  {
+    std::string tmp;
+    if(type2smv(type.subtype(), tmp)) return true;
+    code="array ";
+    code+="..";
+    code+=" of ";
+    code+=tmp;
+  }
+  else if(type.id()==ID_enum)
+  {
+    const irept &elements=type.find("elements");
+    code="{ ";
+    bool first=true;
+    forall_irep(it, elements.get_sub())
+    {
+      if(first) first=false; else code+=", ";
+      code+=it->id_string();
+    }
+    code+=" }";
+  }
+  else if(type.id()==ID_range)
+  {
+    code=type.get_string(ID_from)+".."+type.get_string(ID_to);
+  }
+  else if(type.id()=="submodule")
+  {
+    code=type.get_string(ID_identifier);
+    const exprt &e=(exprt &)type;
+    if(e.has_operands())
+    {
+      code+='(';
+      bool first=true;
+      forall_operands(it, e)
+      {
+        if(first) first=false; else code+=", ";
+        std::string tmp;
+        expr2smv(*it, tmp);
+        code+=tmp;
+      }
+      code+=')';
+    }
+  }
+  else
+    return true;
+
+  return false;
+}
diff --git a/src/ebmc/smvlang/expr2smv.d b/src/ebmc/smvlang/expr2smv.d
new file mode 100644
index 0000000..71253da
--- /dev/null
+++ b/src/ebmc/smvlang/expr2smv.d
@@ -0,0 +1,6 @@
+expr2smv.o: expr2smv.cpp ../util/lispexpr.h ../util/lispirep.h \
+  ../util/i2string.h ../util/std_expr.h ../util/std_types.h \
+  ../util/expr.h ../util/type.h ../util/location.h ../util/irep.h \
+  ../util/dstring.h ../util/string_container.h ../util/hash_cont.h \
+  ../util/string_hash.h ../util/irep_ids.h ../util/mp_arith.h \
+  ../big-int/bigint.hh expr2smv.h
diff --git a/src/ebmc/smvlang/expr2smv.h b/src/ebmc/smvlang/expr2smv.h
new file mode 100644
index 0000000..580b09d
--- /dev/null
+++ b/src/ebmc/smvlang/expr2smv.h
@@ -0,0 +1,13 @@
+/*******************************************************************\
+
+Module:
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#include "expr.h"
+
+bool expr2smv(const exprt &expr, std::string &code);
+bool type2smv(const typet &type, std::string &code);
+
diff --git a/src/ebmc/smvlang/parser.y b/src/ebmc/smvlang/parser.y
new file mode 100644
index 0000000..c7decde
--- /dev/null
+++ b/src/ebmc/smvlang/parser.y
@@ -0,0 +1,551 @@
+%{
+#include <i2string.h>
+
+#include "smv_parser.h"
+#include "smv_typecheck.h"
+
+#define YYSTYPE unsigned
+#define PARSER smv_parser
+
+#include "y.tab.h"
+
+#define YYMAXDEPTH 200000
+#define YYSTYPE_IS_TRIVIAL 1
+
+/*------------------------------------------------------------------------*/
+
+#define yylineno yysmvlineno
+#define yytext yysmvtext
+
+#define yyerror yysmverror
+int yysmverror(const std::string &error);
+int yylex();
+extern char *yytext;
+
+/*------------------------------------------------------------------------*/
+
+#define mto(x, y) stack(x).move_to_operands(stack(y))
+#define binary(x, y, id, z) { init(x, id); \
+  stack(x).move_to_operands(stack(y), stack(z)); }
+
+/*******************************************************************\
+
+Function: init
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+static void init(exprt &expr)
+{
+  expr.clear();
+  PARSER.set_location(expr);
+}
+
+/*******************************************************************\
+
+Function: init
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+static void init(YYSTYPE &expr)
+{
+  newstack(expr);
+  init(stack(expr));
+}
+
+/*******************************************************************\
+
+Function: init
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+static void init(YYSTYPE &expr, const irep_idt &id)
+{
+  init(expr);
+  stack(expr).id(id);
+}
+
+/*******************************************************************\
+
+Function: j_binary
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+static void j_binary(YYSTYPE &dest, YYSTYPE &op1,
+                     const irep_idt &id, YYSTYPE &op2)
+{
+  if(stack(op1).id()==id)
+  {
+    dest=op1;
+    mto(dest, op2);
+  }
+  else if(stack(op2).id()==id)
+  {
+    dest=op2;
+    mto(dest, op1);
+  }
+  else
+    binary(dest, op1, id, op2);
+}
+
+/*******************************************************************\
+
+Function: new_module
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+static void new_module(YYSTYPE &module)
+{
+  const std::string name=smv_module_symbol(stack(module).id_string());
+  PARSER.module=&PARSER.parse_tree.modules[name];
+  PARSER.module->name=name;
+  PARSER.module->base_name=stack(module).id_string();
+  PARSER.module->used=true;
+}
+
+/*------------------------------------------------------------------------*/
+
+%}
+
+%token AG_Token AX_Token AF_Token
+
+%token INIT_Token TRANS_Token SPEC_Token VAR_Token DEFINE_Token ASSIGN_Token
+%token INVAR_Token FAIRNESS_Token MODULE_Token ARRAY_Token OF_Token
+%token DOTDOT_Token BOOLEAN_Token EXTERN_Token
+
+%token NEXT_Token INC_Token DEC_Token CASE_Token ESAC_Token BECOMES_Token
+%token ADD_Token SUB_Token SWITCH_Token init_Token PLUS_Token
+
+%token STRING_Token QSTRING_Token QUOTE_Token
+%token NUMBER_Token
+
+%right IMPLIES_Token
+%left  UNION_Token
+%left  EQUIV_Token
+%left  XOR_Token
+%left  OR_Token
+%left  AND_Token
+%left  NOT_Token
+%left  EX_Token AX_Token EF_Token AF_Token EG_Token AG_Token E_Token A_Token UNTIL_Token
+%left  EQUAL_Token NOTEQUAL_Token LT_Token GT_Token LE_Token GE_Token
+%left  PLUS_Token MINUS_Token
+%left  TIMES_Token DIVIDE_Token
+%left  UMINUS           /* supplies precedence for unary minus */
+%left  DOT_Token
+
+%%
+
+start      : modules
+           | formula { PARSER.module->add_spec(stack($1));
+                       PARSER.module->used=true; }
+           ;
+
+modules    : module
+           | modules module
+           ;
+
+module     : module_head sections
+           ;
+
+module_name: STRING_Token
+           | QUOTE_Token
+           ;
+
+module_head: MODULE_Token module_name { new_module($2); }
+           | MODULE_Token module_name { new_module($2); } '(' module_argument_list_opt ')'
+           ;
+
+sections   : /* epsilon */
+           | section sections
+           ;
+           
+semi_opt   :    /* empty */
+           | ';'
+           ;
+
+section    : VAR_Token vardecls
+           | VAR_Token
+           | INIT_Token formula semi_opt { PARSER.module->add_init(stack($2), stack($1).location()); }
+           | INIT_Token
+           | TRANS_Token formula semi_opt { PARSER.module->add_trans(stack($2), stack($1).location()); }
+           | TRANS_Token
+           | SPEC_Token formula semi_opt { PARSER.module->add_spec(stack($2), stack($1).location()); }
+           | SPEC_Token
+           | ASSIGN_Token assignments
+           | ASSIGN_Token
+           | DEFINE_Token defines
+           | DEFINE_Token
+           | INVAR_Token formula semi_opt { PARSER.module->add_invar(stack($2), stack($1).location()); }
+           | INVAR_Token
+           | FAIRNESS_Token formula semi_opt { PARSER.module->add_fairness(stack($2), stack($1).location()); }
+           | FAIRNESS_Token
+           | EXTERN_Token extern_var semi_opt
+           | EXTERN_Token
+           ;
+ 
+extern_var : variable_name EQUAL_Token QUOTE_Token
+{
+  const irep_idt &identifier=stack($1).get(ID_identifier);
+  smv_parse_treet::mc_vart &var=PARSER.module->vars[identifier];
+
+  if(var.identifier!="")
+  {
+    yyerror("variable `"+id2string(identifier)+"' already declared extern");
+    YYERROR;
+  }
+  else
+    var.identifier=stack($3).id_string();
+}
+           ;
+
+vardecls   : vardecl
+           | vardecl vardecls
+           ;
+
+module_argument: variable_name
+{
+  const irep_idt &identifier=stack($1).get(ID_identifier);
+  smv_parse_treet::mc_vart &var=PARSER.module->vars[identifier];
+  var.var_class=smv_parse_treet::mc_vart::ARGUMENT;
+  PARSER.module->ports.push_back(identifier);
+}
+           ;
+
+module_argument_list: module_argument
+           | module_argument_list ',' module_argument
+           ;
+
+module_argument_list_opt: /* empty */
+           | module_argument_list
+           ;
+
+type       : ARRAY_Token NUMBER_Token DOTDOT_Token NUMBER_Token OF_Token type
+{
+  init($$, ID_array);
+  int start=atoi(stack($2).id().c_str());
+  int end=atoi(stack($4).id().c_str());
+
+  if(end < start)
+  {
+    yyerror("array must end with number >= `"+i2string(start)+"'");
+    YYERROR;
+  }
+
+  stack($$).set(ID_size, end-start+1);
+  stack($$).set(ID_offset, start);
+  stack($$).set(ID_subtype, stack($6));
+}
+           | BOOLEAN_Token { init($$, ID_bool); }
+           | '{' enum_list '}' { $$=$2; }
+           | NUMBER_Token DOTDOT_Token NUMBER_Token
+            {
+              init($$, ID_range);
+              stack($$).set(ID_from, stack($1));
+              stack($$).set(ID_to, stack($3));
+            }
+           | usertype
+           ;
+
+usertype   : module_name
+            {
+              init($$, "submodule");
+              stack($$).set(ID_identifier,
+                            smv_module_symbol(stack($1).id_string()));
+            }
+           | module_name '(' formula_list ')'
+            {
+              init($$, "submodule");
+              stack($$).set(ID_identifier,
+                            smv_module_symbol(stack($1).id_string()));
+              stack($$).operands().swap(stack($3).operands());
+            }
+           ;
+
+enum_list  : enum_element
+              {
+               init($$, ID_enum);
+               stack($$).add("elements").get_sub().push_back(irept(stack($1).id()));
+              }
+           | enum_list ',' enum_element
+              {
+               $$=$1;
+               stack($$).add("elements").get_sub().push_back(irept(stack($3).id())); 
+              }
+           ;
+
+enum_element: STRING_Token
+              {
+                $$=$1;
+                PARSER.module->enum_set.insert(stack($1).id_string());
+              }
+            ;
+
+vardecl    : variable_name ':' type ';'
+{
+  const irep_idt &identifier=stack($1).get(ID_identifier);
+  smv_parse_treet::mc_vart &var=PARSER.module->vars[identifier];
+
+  switch(var.var_class)
+  {
+  case smv_parse_treet::mc_vart::UNKNOWN:
+    var.type=(typet &)stack($3);
+    var.var_class=smv_parse_treet::mc_vart::DECLARED;
+    break;
+
+  case smv_parse_treet::mc_vart::DEFINED:
+    yyerror("variable `"+id2string(identifier)+"' already defined");
+    YYERROR;
+    break;
+
+  case smv_parse_treet::mc_vart::DECLARED:
+    yyerror("variable `"+id2string(identifier)+"' already declared as variable");
+    YYERROR;
+    break;
+  
+  case smv_parse_treet::mc_vart::ARGUMENT:
+    yyerror("variable `"+id2string(identifier)+"' already declared as argument");
+    YYERROR;
+    break;
+  
+  default:
+    assert(false);
+  }
+}
+           ;
+
+assignments: assignment
+           | assignment assignments
+           | define
+           | define assignments
+           ;
+
+assignment : assignment_head '(' assignment_var ')' BECOMES_Token formula ';'
+{
+  binary($$, $3, ID_equal, $6);
+
+  if(stack($1).id()=="next")
+  {
+    exprt &op=stack($$).op0();
+    exprt tmp("smv_next");
+    tmp.operands().resize(1);
+    tmp.op0().swap(op);
+    tmp.swap(op);
+    PARSER.module->add_trans(stack($$));
+  }
+  else
+    PARSER.module->add_init(stack($$));
+}
+;
+
+assignment_var: variable_name
+              ;
+
+assignment_head: init_Token { init($$, ID_init); }
+               | NEXT_Token { init($$, "next"); }
+               ;
+
+defines: define
+       | define defines
+       ;
+
+define : assignment_var BECOMES_Token formula ';'
+{
+  const irep_idt &identifier=stack($1).get(ID_identifier);
+  smv_parse_treet::mc_vart &var=PARSER.module->vars[identifier];
+
+  switch(var.var_class)
+  {
+  case smv_parse_treet::mc_vart::UNKNOWN:
+    var.type.make_nil();
+    var.var_class=smv_parse_treet::mc_vart::DEFINED;
+    break;
+
+  case smv_parse_treet::mc_vart::DECLARED:
+    var.var_class=smv_parse_treet::mc_vart::DEFINED;
+    break;
+
+  case smv_parse_treet::mc_vart::DEFINED:
+    yyerror("variable `"+id2string(identifier)+"' already defined");
+    YYERROR;
+    break;
+  
+  case smv_parse_treet::mc_vart::ARGUMENT:
+    yyerror("variable `"+id2string(identifier)+"' already declared as argument");
+    YYERROR;
+    break;
+  
+  default:
+    assert(false);
+  }
+
+  binary($$, $1, ID_equal, $3);
+  PARSER.module->add_define(stack($$));
+}
+;
+
+formula : term
+        ;
+
+term: variable_name
+    | NEXT_Token '(' term ')' { init($$, "smv_next"); mto($$, $3); }
+    | '(' formula ')' { $$=$2; }
+    | '{' formula_list '}' { $$=$2; stack($$).id("smv_nondet_choice"); }
+    | INC_Token '(' term ')' { init($$, "inc"); mto($$, $3); }
+    | DEC_Token '(' term ')' { init($$, "dec"); mto($$, $3); }
+    | ADD_Token '(' term ',' term ')' { j_binary($$, $3, ID_plus, $5); }
+    | SUB_Token '(' term ',' term ')' { init($$, ID_minus); mto($$, $3); mto($$, $5); }
+    | NUMBER_Token { init($$, "number_constant"); stack($$).set(ID_value, stack($1).id()); }
+    | CASE_Token cases ESAC_Token { $$=$2; }
+    | SWITCH_Token '(' variable_name ')' '{' switches '}' { init($$, "switch"); mto($$, $3); mto($$, $6); }
+    | MINUS_Token term %prec UMINUS { init($$, ID_unary_minus); mto($$, $2); }
+    | term PLUS_Token term    { j_binary($$, $1, ID_plus, $3); }
+    | term MINUS_Token term   { j_binary($$, $1, ID_minus, $3); }
+    | term EQUIV_Token term   { binary($$, $1, ID_equal, $3); }
+    | term IMPLIES_Token term { binary($$, $1, ID_implies, $3); }
+    | term XOR_Token term     { j_binary($$, $1, ID_xor, $3); }
+    | term OR_Token term      { j_binary($$, $1, ID_or, $3); }
+    | term AND_Token term     { j_binary($$, $1, ID_and, $3); }
+    | NOT_Token term          { init($$, ID_not); mto($$, $2); }
+    | AX_Token  term          { init($$, ID_AX);  mto($$, $2); }
+    | AF_Token  term          { init($$, ID_AF);  mto($$, $2); }
+    | AG_Token  term          { init($$, ID_AG);  mto($$, $2); }
+    | term EQUAL_Token    term { binary($$, $1, ID_equal,  $3); }
+    | term NOTEQUAL_Token term { binary($$, $1, ID_notequal, $3); }
+    | term LT_Token       term { binary($$, $1, ID_lt,  $3); }
+    | term LE_Token       term { binary($$, $1, ID_le, $3); }
+    | term GT_Token       term { binary($$, $1, ID_gt,  $3); }
+    | term GE_Token       term { binary($$, $1, ID_ge, $3); }
+    | term UNION_Token    term { binary($$, $1, "smv_union", $3); }
+    ;
+
+formula_list: formula { init($$); mto($$, $1); }
+            | formula_list ',' formula { $$=$1; mto($$, $3); }
+            ;
+
+variable_name: qstring_list
+		{
+                 const irep_idt &id=stack($1).id();
+
+                 bool is_enum=(PARSER.module->enum_set.find(id)!=
+                               PARSER.module->enum_set.end());
+                 bool is_var=(PARSER.module->vars.find(id)!=
+                              PARSER.module->vars.end());
+
+                 if(is_var && is_enum)
+                  {
+                   yyerror("identifier `"+id2string(id)+"' is ambiguous");
+                   YYERROR;
+                  }
+                 else if(is_enum)
+                  {
+                   init($$, "enum_constant");
+                   stack($$).type()=typet(ID_enum);
+                   stack($$).set(ID_value, stack($1).id());
+                  }
+                 else // not an enum, probably a variable
+                  {
+                   init($$, ID_symbol);
+                   stack($$).set(ID_identifier, stack($1).id());
+                   //PARSER.module->vars[stack($1).id()];
+                  }
+                }
+             | QUOTE_Token
+		{
+                 const irep_idt &id=stack($1).id();
+
+                 init($$, ID_symbol);
+                 stack($$).set(ID_identifier, id);
+                 PARSER.module->vars[id];
+                }
+             ;
+
+qstring_list: QSTRING_Token
+              {
+                init($$, std::string(stack($1).id_string(), 1)); // remove backslash
+              }
+            | STRING_Token
+            | qstring_list DOT_Token QSTRING_Token
+              {
+                std::string id(stack($1).id_string());
+                id+=".";
+                id+=std::string(stack($3).id_string(), 1); // remove backslash
+                init($$, id);
+              }
+            | qstring_list DOT_Token STRING_Token
+              {
+                std::string id(stack($1).id_string());
+                id+=".";
+                id+=stack($3).id_string();
+                init($$, id);
+              }
+            | qstring_list '[' NUMBER_Token ']'
+              {
+                std::string id(stack($1).id_string());
+                id+="[";
+                id+=stack($3).id_string();
+                id+="]";
+                init($$, id);
+              }
+            | qstring_list '(' NUMBER_Token ')'
+              {
+                std::string id(stack($1).id_string());
+                id+="(";
+                id+=stack($3).id_string();
+                id+=")";
+                init($$, id);
+              }
+            ;
+
+cases   : { init($$, "smv_cases"); }
+        | cases case { $$=$1; mto($$, $2); }
+        ;
+
+case    : formula ':' formula ';' { binary($$, $1, ID_case, $3); }
+        ;
+
+switches: { init($$, "switches"); }
+        | switches switch { $$=$1; mto($$, $2); }
+        ;
+
+switch  : NUMBER_Token ':' term ';' { init($$, "switch"); mto($$, $1); mto($$, $3); }
+        ;
+
+%%
+
+int yysmverror(const std::string &error)
+{
+  PARSER.parse_error(error, yytext);
+  return 0;
+}
+
+#undef yyerror
+
diff --git a/src/ebmc/smvlang/scanner.l b/src/ebmc/smvlang/scanner.l
new file mode 100644
index 0000000..b57a76b
--- /dev/null
+++ b/src/ebmc/smvlang/scanner.l
@@ -0,0 +1,133 @@
+%option nounput
+
+%{
+#ifdef _WIN32
+#define YY_NO_UNISTD_H
+static int isatty(int) { return 0; }
+#endif
+
+#include <stdio.h>
+#include <string.h>
+
+#include <expr.h>
+
+#define PARSER smv_parser
+#define YYSTYPE unsigned
+
+#include "smv_parser.h"
+#include "y.tab.h"
+
+int yysmverror(const std::string &error);
+
+void newlocation(YYSTYPE &x)
+{
+  newstack(x);
+  PARSER.set_location(stack(x));
+}
+
+%}
+
+%pointer
+
+%%
+
+"/*"		{
+		  int c;
+
+		  for(;;)
+		    {
+		      while((c = yyinput()) != '*' && c != EOF)
+			;
+
+		      if(c == '*')
+                        {
+			  while((c = yyinput()) == '*')
+                            ;
+
+			  if( c == '/' ) break;
+                        }
+
+		      if (c == EOF)
+                        {
+			  yysmverror("EOF in comment");
+			  break;
+                        }
+                    }
+                }
+
+"//".*          ;
+"--".*          ;
+"#".*		{ /* preprocessor */ }
+
+[ \t\n]+	;
+
+"INIT"		{ newlocation(yysmvlval); return INIT_Token; }
+"TRANS"		{ newlocation(yysmvlval); return TRANS_Token; }
+"SPEC"		{ newlocation(yysmvlval); return SPEC_Token; }
+"INVAR"		{ newlocation(yysmvlval); return INVAR_Token; }
+"VAR"		{ newlocation(yysmvlval); return VAR_Token; }
+"ASSIGN"	{ newlocation(yysmvlval); return ASSIGN_Token; }
+"DEFINE"	{ newlocation(yysmvlval); return DEFINE_Token; }
+"FAIRNESS"	{ newlocation(yysmvlval); return FAIRNESS_Token; }
+"MODULE"	{ newlocation(yysmvlval); return MODULE_Token; }
+"EXTERN"	{ newlocation(yysmvlval); return EXTERN_Token; }
+
+"AG"		return AG_Token;
+"AF"		return AF_Token;
+"AX"		return AX_Token;
+"next"		return NEXT_Token;
+"init"		return init_Token;
+"case"		return CASE_Token;
+"esac"		return ESAC_Token;
+"switch"	return SWITCH_Token;
+"array"		return ARRAY_Token;
+"of"		return OF_Token;
+"boolean"	return BOOLEAN_Token;
+"union"		return UNION_Token;
+".."		return DOTDOT_Token;
+"XOR"		return XOR_Token;
+
+[\$A-Za-z_][A-Za-z0-9_\$#-]*	{
+                  newstack(yysmvlval);
+                  stack(yysmvlval).id(yytext);
+		  return STRING_Token;
+		}
+\\[A-Za-z0-9_\$#-]*	{
+                  newstack(yysmvlval);
+                  stack(yysmvlval).id(yytext);
+		  return QSTRING_Token;
+		}
+[0-9][0-9]*	{
+                  newstack(yysmvlval);
+                  stack(yysmvlval).id(yytext);
+		  return NUMBER_Token;
+		}
+\"[^\"]*\"      {
+                  newstack(yysmvlval);
+                  std::string tmp(yytext);
+                  stack(yysmvlval).id(std::string(tmp, 1, tmp.size()-2));
+                  return QUOTE_Token;
+                }
+
+"~"		return NOT_Token;
+"!"		return NOT_Token;
+"+"		return PLUS_Token;
+"-"		return MINUS_Token;
+"|"		return OR_Token;
+"&"		return AND_Token;
+"->"		return IMPLIES_Token;
+"<->"		return EQUIV_Token;
+"="		return EQUAL_Token;
+"<="		return LE_Token;
+">="		return GE_Token;
+"<"		return LT_Token;
+">"		return GT_Token;
+"!="		return NOTEQUAL_Token;
+":="		return BECOMES_Token;
+"."		return DOT_Token;
+
+.		return yytext[0];
+
+%%
+
+int yywrap() { return 1; }
diff --git a/src/ebmc/smvlang/smv_language.cpp b/src/ebmc/smvlang/smv_language.cpp
new file mode 100644
index 0000000..84770c4
--- /dev/null
+++ b/src/ebmc/smvlang/smv_language.cpp
@@ -0,0 +1,265 @@
+/*******************************************************************\
+
+Module:
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#include "smv_language.h"
+#include "smv_typecheck.h"
+#include "smv_parser.h"
+#include "expr2smv.h"
+
+/*******************************************************************\
+
+Function: smv_languaget::parse
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+bool smv_languaget::parse(
+  std::istream &instream,
+  const std::string &path,
+  message_handlert &message_handler)
+{
+  smv_parser.clear();
+
+  const std::string main_name=smv_module_symbol("main");
+  smv_parser.module=&smv_parser.parse_tree.modules[main_name];
+  smv_parser.module->name=main_name;
+  smv_parser.module->base_name="main";
+
+  smv_parser.filename=path;
+  smv_parser.in=&instream;
+  smv_parser.set_message_handler(message_handler);
+
+  bool result=smv_parser.parse();
+
+  // see if we used main
+
+  if(!smv_parser.parse_tree.modules[main_name].used)
+    smv_parser.parse_tree.modules.erase(main_name);
+
+  smv_parse_tree.swap(smv_parser.parse_tree);
+
+  // save some memory
+  smv_parser.clear();
+
+  return result;
+}
+
+/*******************************************************************\
+
+Function: smv_languaget::dependencies
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void smv_languaget::dependencies(
+  const std::string &module, 
+  std::set<std::string> &module_set)
+{
+  smv_parse_treet::modulest::const_iterator
+    m_it=smv_parse_tree.modules.find(module);
+
+  if(m_it==smv_parse_tree.modules.end()) return;
+
+  const smv_parse_treet::modulet &smv_module=m_it->second;
+
+  for(smv_parse_treet::mc_varst::const_iterator it=smv_module.vars.begin();
+      it!=smv_module.vars.end(); it++)
+    if(it->second.type.id()=="submodule")
+      module_set.insert(it->second.type.get_string("identifier"));
+}
+
+/*******************************************************************\
+
+Function: smv_languaget::modules_provided
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void smv_languaget::modules_provided(std::set<std::string> &module_set)
+{
+  for(smv_parse_treet::modulest::const_iterator
+      it=smv_parse_tree.modules.begin();
+      it!=smv_parse_tree.modules.end(); it++)
+    module_set.insert(id2string(it->second.name));
+}
+
+/*******************************************************************\
+
+Function: smv_languaget::typecheck
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+bool smv_languaget::typecheck(
+  contextt &context,
+  const std::string &module,
+  message_handlert &message_handler)
+{
+  return smv_typecheck(smv_parse_tree, context, module, message_handler);
+}
+
+/*******************************************************************\
+
+Function: smv_languaget::show_parse
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+  
+void smv_languaget::show_parse(std::ostream &out)
+{
+  for(smv_parse_treet::modulest::const_iterator
+      it=smv_parse_tree.modules.begin();
+      it!=smv_parse_tree.modules.end(); it++)
+  {
+    const smv_parse_treet::modulet &module=it->second;
+    out << "Module: " << module.name << std::endl << std::endl;
+
+    out << "  VARIABLES:" << std::endl;
+
+    for(smv_parse_treet::mc_varst::const_iterator it=module.vars.begin();
+        it!=module.vars.end(); it++)
+      if(it->second.type.id()!="submodule")
+      {
+        std::string msg;
+        type2smv(it->second.type, msg);
+        out << "    " << it->first << ": " 
+            << msg << ";" << std::endl;
+      }
+
+    out << std::endl;
+
+    out << "  SUBMODULES:" << std::endl;
+
+    for(smv_parse_treet::mc_varst::const_iterator
+        it=module.vars.begin();
+        it!=module.vars.end(); it++)
+      if(it->second.type.id()=="submodule")
+      {
+        std::string msg;
+        type2smv(it->second.type, msg);
+        out << "    " << it->first << ": " 
+            << msg << ";" << std::endl;
+      }
+
+    out << std::endl;
+
+    out << "  ITEMS:" << std::endl;
+
+    forall_item_list(it, module.items)
+    {
+      out << "    TYPE: " << to_string(it->item_type) << std::endl;
+      out << "    EXPR: " << it->expr << std::endl;
+      out << std::endl;
+    }
+  }
+}
+
+/*******************************************************************\
+
+Function: smv_languaget::from_expr
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+bool smv_languaget::from_expr(const exprt &expr, std::string &code,
+                              const namespacet &ns)
+{
+  return expr2smv(expr, code);
+}
+
+/*******************************************************************\
+
+Function: smv_languaget::from_type
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+bool smv_languaget::from_type(
+  const typet &type,
+  std::string &code,
+  const namespacet &ns)
+{
+  return type2smv(type, code);
+}
+
+/*******************************************************************\
+
+Function: smv_languaget::to_expr
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+bool smv_languaget::to_expr(
+  const std::string &code,
+  const std::string &module,
+  exprt &expr,
+  message_handlert &message_handler,
+  const namespacet &ns)
+{
+  messaget message(message_handler);
+  message.error("not yet implemented");
+  return true;
+}
+
+/*******************************************************************\
+
+Function: new_smv_language
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+  
+languaget *new_smv_language()
+{
+  return new smv_languaget;
+}
+
diff --git a/src/ebmc/smvlang/smv_language.d b/src/ebmc/smvlang/smv_language.d
new file mode 100644
index 0000000..3de0cbb
--- /dev/null
+++ b/src/ebmc/smvlang/smv_language.d
@@ -0,0 +1,8 @@
+smv_language.o: smv_language.cpp smv_language.h ../util/language.h \
+  smv_parse_tree.h ../util/hash_cont.h ../util/string_hash.h \
+  ../util/expr.h ../util/type.h ../util/location.h ../util/irep.h \
+  ../util/dstring.h ../util/string_container.h ../util/hash_cont.h \
+  ../util/string_hash.h ../util/irep_ids.h smv_typecheck.h \
+  ../util/context.h ../util/symbol.h ../util/message.h ../util/location.h \
+  smv_parser.h ../util/parser.h ../util/expr.h ../util/message.h \
+  expr2smv.h
diff --git a/src/ebmc/smvlang/smv_language.h b/src/ebmc/smvlang/smv_language.h
new file mode 100644
index 0000000..12b6cb6
--- /dev/null
+++ b/src/ebmc/smvlang/smv_language.h
@@ -0,0 +1,75 @@
+/*******************************************************************\
+
+Module:
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#ifndef CPROVER_SMV_LANGUAGE_H
+#define CPROVER_SMV_LANGUAGE_H
+
+/*! \defgroup gr_smvlang SMV front-end */
+
+#include <language.h>
+
+#include "smv_parse_tree.h"
+
+/*! \brief TO_BE_DOCUMENTED
+    \ingroup gr_smvlang
+*/
+class smv_languaget:public languaget
+{
+public:
+  virtual bool parse(
+    std::istream &instream,
+    const std::string &path,
+    message_handlert &message_handler);
+
+  virtual void dependencies(
+    const std::string &module,
+    std::set<std::string> &module_set);
+
+  virtual void modules_provided(
+    std::set<std::string> &module_set);
+                 
+  virtual bool typecheck(
+    contextt &context,
+    const std::string &module,
+    message_handlert &message_handler);
+  
+  virtual void show_parse(std::ostream &out);
+  
+  virtual ~smv_languaget() { }
+  
+  virtual bool from_expr(
+    const exprt &expr,
+    std::string &code,
+    const namespacet &ns);
+
+  virtual bool from_type(
+    const typet &type,
+    std::string &code,
+    const namespacet &ns);
+
+  virtual bool to_expr(
+    const std::string &code,
+    const std::string &module,
+    exprt &expr,
+    message_handlert &message_handler,
+    const namespacet &ns);
+                       
+  virtual std::string id() const { return "SMV"; }
+  virtual std::string description() const { return "SMV"; }
+  virtual std::set<std::string> extensions() const
+  { std::set<std::string> s; s.insert("smv"); return s; }
+  
+  virtual languaget *new_language()
+  { return new smv_languaget; }
+     
+  smv_parse_treet smv_parse_tree;
+};
+
+languaget *new_smv_language();
+ 
+#endif
diff --git a/src/ebmc/smvlang/smv_parse_tree.cpp b/src/ebmc/smvlang/smv_parse_tree.cpp
new file mode 100644
index 0000000..d184634
--- /dev/null
+++ b/src/ebmc/smvlang/smv_parse_tree.cpp
@@ -0,0 +1,72 @@
+/*******************************************************************\
+
+Module: SMV Parse Tree
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#include "smv_parse_tree.h"
+
+/*******************************************************************\
+
+Function: smv_parse_treet::swap
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void smv_parse_treet::swap(smv_parse_treet &smv_parse_tree)
+{
+  smv_parse_tree.modules.swap(modules);
+}
+
+/*******************************************************************\
+
+Function: smv_parse_treet::clear
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void smv_parse_treet::clear()
+{
+  modules.clear();
+}
+
+/*******************************************************************\
+
+Function: operator <<
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+std::string to_string(smv_parse_treet::modulet::itemt::item_typet i)
+{
+  switch(i)
+  {
+  case smv_parse_treet::modulet::itemt::INVAR:    return "INVAR";
+  case smv_parse_treet::modulet::itemt::TRANS:    return "TRANS";
+  case smv_parse_treet::modulet::itemt::INIT:     return "INIT";
+  case smv_parse_treet::modulet::itemt::SPEC:     return "SPEC";
+  case smv_parse_treet::modulet::itemt::FAIRNESS: return "FAIRNESS";
+  case smv_parse_treet::modulet::itemt::DEFINE:    return "DEFINE";  
+  
+  default:;
+  }
+  
+  return "";
+}
diff --git a/src/ebmc/smvlang/smv_parse_tree.d b/src/ebmc/smvlang/smv_parse_tree.d
new file mode 100644
index 0000000..61be4dd
--- /dev/null
+++ b/src/ebmc/smvlang/smv_parse_tree.d
@@ -0,0 +1,4 @@
+smv_parse_tree.o: smv_parse_tree.cpp smv_parse_tree.h ../util/hash_cont.h \
+  ../util/string_hash.h ../util/expr.h ../util/type.h ../util/location.h \
+  ../util/irep.h ../util/dstring.h ../util/string_container.h \
+  ../util/hash_cont.h ../util/string_hash.h ../util/irep_ids.h
diff --git a/src/ebmc/smvlang/smv_parse_tree.h b/src/ebmc/smvlang/smv_parse_tree.h
new file mode 100644
index 0000000..b25abf5
--- /dev/null
+++ b/src/ebmc/smvlang/smv_parse_tree.h
@@ -0,0 +1,175 @@
+/*******************************************************************\
+
+Module: SMV Parse Tree
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#ifndef CPROVER_SMV_PARSE_TREE_H
+#define CPROVER_SMV_PARSE_TREE_H
+
+#include <hash_cont.h>
+#include <string_hash.h>
+#include <expr.h>
+
+class smv_parse_treet
+{
+public:
+
+  struct mc_vart
+  {
+    typedef enum { UNKNOWN, DECLARED, DEFINED, ARGUMENT } var_classt;
+    var_classt var_class;
+    typet type;
+    irep_idt identifier;
+    
+    mc_vart():var_class(UNKNOWN), type(typet(ID_bool))
+    {
+    }
+  };
+   
+  typedef hash_map_cont<irep_idt, mc_vart, irep_id_hash> mc_varst;
+  typedef hash_set_cont<irep_idt, irep_id_hash> enum_sett;
+
+  struct modulet
+  {
+    irep_idt name, base_name;
+    
+    struct itemt
+    {
+      enum item_typet { SPEC, INIT, TRANS, DEFINE, INVAR, FAIRNESS };
+      
+      friend std::string to_string(item_typet i);
+      
+      item_typet item_type;
+      exprt expr;
+      locationt location;
+
+      bool is_spec() const
+      {
+        return item_type==SPEC;
+      }
+      
+      bool is_define() const
+      {
+        return item_type==DEFINE;
+      }
+      
+      bool is_invar() const
+      {
+        return item_type==INVAR;
+      }
+      
+      bool is_trans() const
+      {
+        return item_type==TRANS;
+      }
+      
+      bool is_init() const
+      {
+        return item_type==INIT;
+      }
+      
+    };
+    
+    typedef std::list<itemt> item_listt;
+    item_listt items;
+    
+    void add_item(
+      itemt::item_typet item_type,
+      const exprt &expr,
+      const locationt &location)
+    {
+      items.push_back(itemt());
+      items.back().item_type=item_type;
+      items.back().expr=expr;
+      items.back().location=location;
+    }
+    
+    void add_invar(const exprt &expr)
+    {
+      add_item(itemt::INVAR, expr, static_cast<const locationt &>(get_nil_irep()));
+    }
+    
+    void add_spec(const exprt &expr)
+    {
+      add_item(itemt::SPEC, expr, static_cast<const locationt &>(get_nil_irep()));
+    }
+    
+    void add_define(const exprt &expr)
+    {
+      add_item(itemt::DEFINE, expr, static_cast<const locationt &>(get_nil_irep()));
+    }
+    
+    void add_fairness(const exprt &expr)
+    {
+      add_item(itemt::FAIRNESS, expr, static_cast<const locationt &>(get_nil_irep()));
+    }
+    
+    void add_init(const exprt &expr)
+    {
+      add_item(itemt::INIT, expr, static_cast<const locationt &>(get_nil_irep()));
+    }
+    
+    void add_trans(const exprt &expr)
+    {
+      add_item(itemt::TRANS, expr, static_cast<const locationt &>(get_nil_irep()));
+    }
+    
+    void add_invar(const exprt &expr, const locationt &location)
+    {
+      add_item(itemt::INVAR, expr, location);
+    }
+    
+    void add_spec(const exprt &expr, const locationt &location)
+    {
+      add_item(itemt::SPEC, expr, location);
+    }
+    
+    void add_define(const exprt &expr, const locationt &location)
+    {
+      add_item(itemt::DEFINE, expr, location);
+    }
+    
+    void add_fairness(const exprt &expr, const locationt &location)
+    {
+      add_item(itemt::FAIRNESS, expr, location);
+    }
+    
+    void add_init(const exprt &expr, const locationt &location)
+    {
+      add_item(itemt::INIT, expr, location);
+    }
+    
+    void add_trans(const exprt &expr, const locationt &location)
+    {
+      add_item(itemt::TRANS, expr, location);
+    }
+    
+    mc_varst vars;
+    enum_sett enum_set;
+    bool used;
+    
+    std::list<irep_idt> ports;
+    
+    modulet():used(false) { }
+  };
+   
+  typedef hash_map_cont<irep_idt, modulet, irep_id_hash> modulest;
+  
+  modulest modules;
+  
+  void swap(smv_parse_treet &smv_parse_tree);
+  void clear();
+};
+
+#define forall_item_list(it, expr) \
+  for(smv_parse_treet::modulet::item_listt::const_iterator it=(expr).begin(); \
+      it!=(expr).end(); it++)
+
+#define Forall_item_list(it, expr) \
+  for(smv_parse_treet::modulet::item_listt::iterator it=(expr).begin(); \
+      it!=(expr).end(); it++)
+
+#endif
diff --git a/src/ebmc/smvlang/smv_parser.cpp b/src/ebmc/smvlang/smv_parser.cpp
new file mode 100644
index 0000000..ef9a33e
--- /dev/null
+++ b/src/ebmc/smvlang/smv_parser.cpp
@@ -0,0 +1,12 @@
+/*******************************************************************\
+
+Module: SMV Parse Tree
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#include "smv_parser.h"
+
+smv_parsert smv_parser;
+
diff --git a/src/ebmc/smvlang/smv_parser.d b/src/ebmc/smvlang/smv_parser.d
new file mode 100644
index 0000000..85894ac
--- /dev/null
+++ b/src/ebmc/smvlang/smv_parser.d
@@ -0,0 +1,6 @@
+smv_parser.o: smv_parser.cpp smv_parser.h ../util/parser.h ../util/expr.h \
+  ../util/type.h ../util/location.h ../util/irep.h ../util/dstring.h \
+  ../util/string_container.h ../util/hash_cont.h ../util/string_hash.h \
+  ../util/irep_ids.h ../util/message.h ../util/location.h \
+  smv_parse_tree.h ../util/hash_cont.h ../util/string_hash.h \
+  ../util/expr.h
diff --git a/src/ebmc/smvlang/smv_parser.h b/src/ebmc/smvlang/smv_parser.h
new file mode 100644
index 0000000..024f212
--- /dev/null
+++ b/src/ebmc/smvlang/smv_parser.h
@@ -0,0 +1,39 @@
+/*******************************************************************\
+
+Module: SMV Parser
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#ifndef CPROVER_SMV_PARSER_H
+#define CPROVER_SMV_PARSER_H
+
+#include <parser.h>
+
+#include "smv_parse_tree.h"
+
+int yysmvparse();
+
+class smv_parsert:public parsert
+{
+ public:
+  smv_parse_treet parse_tree;
+  smv_parse_treet::modulet *module;
+  
+  virtual bool parse()
+  {
+    return yysmvparse();
+  }
+  
+  virtual void clear()
+  {
+    parsert::clear();
+    parse_tree.clear();
+    module=NULL;
+  }
+};
+
+extern smv_parsert smv_parser;
+
+#endif
diff --git a/src/ebmc/smvlang/smv_typecheck.cpp b/src/ebmc/smvlang/smv_typecheck.cpp
new file mode 100644
index 0000000..6c9ec4e
--- /dev/null
+++ b/src/ebmc/smvlang/smv_typecheck.cpp
@@ -0,0 +1,1466 @@
+/*******************************************************************\
+
+Module: SMV Language Type Checking
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#include <assert.h>
+
+#include <set>
+#include <algorithm>
+
+#include <expr_util.h>
+#include <location.h>
+#include <typecheck.h>
+#include <arith_tools.h>
+#include <i2string.h>
+#include <std_expr.h>
+
+#include "smv_typecheck.h"
+#include "expr2smv.h"
+
+class smv_typecheckt:public typecheckt
+{
+public:
+  smv_typecheckt(
+    smv_parse_treet &_smv_parse_tree,
+    contextt &_context,
+    const std::string &_module,
+    bool _do_spec,
+    message_handlert &_message_handler):
+    typecheckt(_message_handler),
+    smv_parse_tree(_smv_parse_tree),
+    context(_context),
+    module(_module),
+    do_spec(_do_spec)
+  {
+    nondet_count=0;
+  }
+
+  virtual ~smv_typecheckt() { }
+
+  typedef enum { INIT, TRANS, OTHER } modet;
+
+  void convert(smv_parse_treet::modulet &smv_module);
+  void convert(smv_parse_treet::mc_varst &vars);
+
+  void collect_define(const exprt &expr);
+  void convert_defines(exprt &invar);
+  void convert_define(const irep_idt &identifier);
+
+  typedef enum { NORMAL, NEXT } expr_modet;
+  virtual void convert(exprt &exprt, expr_modet expr_mode);
+
+  virtual void typecheck(exprt &exprt, const typet &type, modet mode);
+  virtual void typecheck_op(exprt &exprt, const typet &type, modet mode);
+
+  virtual void typecheck();
+
+  // overload to use SMV syntax
+  
+  virtual std::string to_string(const typet &type);
+  virtual std::string to_string(const exprt &expr);
+
+protected:
+  smv_parse_treet &smv_parse_tree;
+  contextt &context;
+  const std::string &module;
+  bool do_spec;
+
+  class smv_ranget
+  {
+  public:
+    smv_ranget():from(0), to(0)
+    {
+    }
+  
+    mp_integer from, to;
+    
+    bool is_contained_in(const smv_ranget &other) const
+    {
+      if(other.from>from) return false;
+      if(other.to<to) return false;
+      return true;
+    }
+    
+    void make_union(const smv_ranget &other)
+    {
+      mp_min(from, other.from);
+      mp_max(to, other.to);
+    }
+    
+    void to_type(typet &dest) const
+    {
+      dest=typet(ID_range);
+      dest.set(ID_from, integer2string(from));
+      dest.set(ID_to, integer2string(to));
+    }
+    
+    bool is_bool() const
+    {
+      return from==0 && to==1;
+    }
+    
+    bool is_singleton() const
+    {
+      return from==to;
+    }
+  };
+  
+  void convert_type(const typet &type, smv_ranget &dest);
+  void convert(smv_parse_treet::modulet::itemt &item);
+  void typecheck(smv_parse_treet::modulet::itemt &item);
+
+  smv_parse_treet::modulet *modulep;
+
+  unsigned nondet_count;
+
+  void flatten_hierarchy(smv_parse_treet::modulet &module);
+
+  void instantiate(
+    smv_parse_treet::modulet &smv_module,
+    const irep_idt &identifier,
+    const irep_idt &instance,
+    const exprt::operandst &operands,
+    const irept &location);
+    
+  void type_union(
+    const typet &type1,
+    const typet &type2,
+    typet &dest);
+
+  typedef std::map<irep_idt, exprt> rename_mapt;
+
+  void instantiate_rename(exprt &expr,
+                          const rename_mapt &rename_map);
+
+  void convert_ports(smv_parse_treet::modulet &smv_module,
+                     typet &dest);
+
+  // for defines
+  class definet
+  {
+  public:
+    exprt value;
+    bool typechecked, in_progress;
+    
+    explicit definet(const exprt &_v):value(_v), typechecked(false), in_progress(false)
+    {
+    }
+
+    definet():typechecked(false), in_progress(false)
+    {
+    }
+  };
+  
+  typedef hash_map_cont<irep_idt, definet, irep_id_hash> define_mapt;
+  define_mapt define_map;
+};
+
+/*******************************************************************\
+
+Function: smv_typecheckt::convert_ports
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void smv_typecheckt::convert_ports(
+  smv_parse_treet::modulet &smv_module,
+  typet &dest)
+{
+  irept::subt &ports=dest.add("ports").get_sub();
+
+  ports.reserve(smv_module.ports.size());
+
+  for(std::list<irep_idt>::const_iterator
+      it=smv_module.ports.begin();
+      it!=smv_module.ports.end();
+      it++)
+  {
+    ports.push_back(exprt(ID_symbol));
+    ports.back().set(ID_identifier,
+      id2string(smv_module.name)+"::var::"+id2string(*it));
+  }
+}
+
+/*******************************************************************\
+
+Function: smv_typecheckt::flatten_hierarchy
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void smv_typecheckt::flatten_hierarchy(smv_parse_treet::modulet &smv_module)
+{
+  for(smv_parse_treet::mc_varst::iterator
+      it=smv_module.vars.begin();
+      it!=smv_module.vars.end();
+      it++)
+  {
+    smv_parse_treet::mc_vart &var=it->second;
+
+    if(var.type.id()=="submodule")
+    {
+      exprt &inst=static_cast<exprt &>(static_cast<irept &>(var.type));
+
+      Forall_operands(o_it, inst)
+        convert(*o_it, NORMAL);
+
+      instantiate(smv_module,
+                  inst.get(ID_identifier),
+                  it->first,
+                  inst.operands(),
+                  inst.find_location());
+    }
+  }
+}
+
+/*******************************************************************\
+
+Function: smv_typecheckt::instantiate
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void smv_typecheckt::instantiate(
+  smv_parse_treet::modulet &smv_module,
+  const irep_idt &identifier,
+  const irep_idt &instance,
+  const exprt::operandst &operands,
+  const irept &location)
+{
+  contextt::symbolst::const_iterator s_it=
+    context.symbols.find(identifier);
+
+  if(s_it==context.symbols.end())
+  {
+    err_location(location);
+    str << "submodule `"
+        << identifier
+        << "' not found";
+    throw 0;
+  }
+
+  if(s_it->second.type.id()!=ID_module)
+  {
+    err_location(location);
+    str << "submodule `"
+        << identifier
+        << "' not a module";
+  }
+
+  const irept::subt &ports=s_it->second.type.find("ports").get_sub();
+
+  // do the arguments/ports
+
+  if(ports.size()!=operands.size())
+  {
+    err_location(location);
+    str << "submodule `" << identifier
+        << "' has wrong number of arguments";
+    throw 0;
+  }
+
+  std::set<irep_idt> port_identifiers;
+  rename_mapt rename_map;
+
+  for(unsigned i=0; i<ports.size(); i++)
+  {
+    const irep_idt &identifier=ports[i].get(ID_identifier);
+    rename_map.insert(std::pair<irep_idt, exprt>(identifier, operands[i]));
+    port_identifiers.insert(identifier);
+  }
+
+  // do the variables
+
+  std::string new_prefix=
+    id2string(smv_module.name)+"::var::"+id2string(instance)+".";
+
+  std::set<irep_idt> var_identifiers;
+
+  forall_symbol_module_map(v_it, context.symbol_module_map, identifier)
+  {
+    contextt::symbolst::const_iterator s_it2=
+      context.symbols.find(v_it->second);
+
+    if(s_it2==context.symbols.end())
+    {
+      str << "symbol `" << v_it->second << "' not found";
+      throw 0;
+    }
+
+    if(port_identifiers.find(s_it2->second.name)!=
+       port_identifiers.end())
+    {
+    }
+    else if(s_it2->second.type.id()==ID_module)
+    {
+    }
+    else
+    {
+      symbolt symbol(s_it2->second);
+
+      symbol.name=new_prefix+id2string(symbol.base_name);
+      symbol.module=smv_module.name;
+
+      rename_map.insert(std::pair<irep_idt, exprt>
+                        (s_it2->second.name, symbol_expr(symbol)));
+
+      var_identifiers.insert(symbol.name);
+
+      context.move(symbol);
+    }
+  }
+
+  // fix values (macros)
+
+  for(std::set<irep_idt>::const_iterator
+      v_it=var_identifiers.begin();
+      v_it!=var_identifiers.end();
+      v_it++)
+  {
+    contextt::symbolst::iterator s_it2=
+      context.symbols.find(*v_it);
+
+    if(s_it2==context.symbols.end())
+    {
+      str << "symbol `" << *v_it << "' not found";
+      throw 0;
+    }
+
+    symbolt &symbol=s_it2->second;
+
+    if(!symbol.value.is_nil())
+    {
+      instantiate_rename(symbol.value, rename_map);
+      typecheck(symbol.value, symbol.type, OTHER);
+    }
+  }
+
+  // get the transition system
+
+  const transt &trans=to_trans_expr(s_it->second.value);
+
+  std::string old_prefix=id2string(s_it->first)+"::var::";
+
+  // do the transition system
+
+  if(!trans.invar().is_true())
+  {
+    exprt tmp(trans.invar());
+    instantiate_rename(tmp, rename_map);
+    smv_module.add_invar(tmp);
+  }
+    
+  if(!trans.init().is_true())
+  {
+    exprt tmp(trans.init());
+    instantiate_rename(tmp, rename_map);
+    smv_module.add_init(tmp);
+  }
+    
+  if(!trans.trans().is_true())
+  {
+    exprt tmp(trans.trans());
+    instantiate_rename(tmp, rename_map);
+    smv_module.add_trans(tmp);
+  }
+
+}
+
+/*******************************************************************\
+
+Function: smv_typecheckt::instantiate_rename
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void smv_typecheckt::instantiate_rename(
+  exprt &expr,
+  const rename_mapt &rename_map)
+{
+  Forall_operands(it, expr)
+    instantiate_rename(*it, rename_map);
+
+  if(expr.id()==ID_symbol || expr.id()==ID_next_symbol)
+  {
+    const irep_idt &old_identifier=expr.get(ID_identifier);
+    bool next=expr.id()==ID_next_symbol;
+
+    rename_mapt::const_iterator it=
+      rename_map.find(old_identifier);
+
+    if(it!=rename_map.end())
+    {
+      expr=it->second;
+
+      if(next)
+      {
+        if(expr.id()==ID_symbol)
+        {
+          expr=it->second;
+          expr.id(ID_next_symbol);
+        }
+        else
+        {
+          err_location(expr);
+          str << "expected symbol expression here, but got "
+              << to_string(it->second);
+          throw 0;
+        }
+      }
+      else
+        expr=it->second;
+    }
+  }
+}
+
+/*******************************************************************\
+
+Function: smv_typecheckt::typecheck_op
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void smv_typecheckt::typecheck_op(
+  exprt &expr,
+  const typet &type,
+  modet mode)
+{
+  if(expr.operands().size()==0)
+  {
+    err_location(expr);
+    str << "Expected operands for " << expr.id_string()
+        << " operator";
+    throw 0;
+  }
+
+  Forall_operands(it, expr)
+    typecheck(*it, type, mode);
+
+  expr.type()=type;
+
+  // type fixed?
+
+  if(type.is_nil())
+  {
+    // figure out types
+
+    forall_operands(it, expr)
+      if(!it->type().is_nil())
+      {
+        expr.type()=it->type();
+        break;
+      }
+  }
+}
+
+/*******************************************************************\
+
+Function: smv_typecheckt::convert_type
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void smv_typecheckt::convert_type(const typet &src, smv_ranget &dest)
+{
+  if(src.id()==ID_bool)
+  {
+    dest.from=0;
+    dest.to=1;
+  }
+  else if(src.id()==ID_range)
+  {
+    dest.from=string2integer(src.get_string(ID_from));
+    dest.to=string2integer(src.get_string(ID_to));
+  }
+  else
+  {
+    err_location(src);
+    str << "Unexpected type: `" << to_string(src) << "'";
+    throw 0;
+  }
+}
+
+/*******************************************************************\
+
+Function: smv_typecheckt::type_union
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void smv_typecheckt::type_union(
+  const typet &type1,
+  const typet &type2,
+  typet &dest)
+{
+  if(type1.is_nil())
+  {
+    dest=type2;
+    return;
+  }
+
+  if(type2.is_nil())
+  {
+    dest=type1;
+    return;
+  }
+
+  smv_ranget range1, range2;
+  convert_type(type1, range1);
+  convert_type(type2, range2);
+
+  range1.make_union(range2);
+  
+  if((type1.id()==ID_bool || type2.id()==ID_bool) &&
+     range1.is_bool())
+  {
+    dest=typet(ID_bool);
+  }
+  else
+    range1.to_type(dest);
+}
+
+/*******************************************************************\
+
+Function: smv_typecheckt::typecheck
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void smv_typecheckt::typecheck(
+  exprt &expr,
+  const typet &type,
+  modet mode)
+{
+  if(expr.id()==ID_symbol || 
+     expr.id()==ID_next_symbol)
+  {
+    const irep_idt &identifier=expr.get(ID_identifier);
+    bool next=expr.id()==ID_next_symbol;
+    
+    if(define_map.find(identifier)!=define_map.end())
+      convert_define(identifier);
+
+    contextt::symbolst::iterator s_it=context.symbols.find(identifier);
+
+    if(s_it==context.symbols.end())
+    {
+      err_location(expr);
+      str << "variable `" << identifier << "' not found";
+      throw 0;
+    }
+
+    symbolt &symbol=s_it->second;
+    
+    assert(symbol.type.is_not_nil());
+    expr.type()=symbol.type;
+
+    if(mode==INIT || (mode==TRANS && next))
+    {
+      if(symbol.module==module)
+      {
+        symbol.is_input=false;
+        symbol.is_statevar=true;
+      }
+    }
+  }
+  else if(expr.id()==ID_and ||
+          expr.id()==ID_or ||
+          expr.id()==ID_xor ||
+          expr.id()==ID_not)
+  {
+    typecheck_op(expr, typet(ID_bool), mode);
+  }
+  else if(expr.id()==ID_nondet_symbol)
+  {
+    if(!type.is_nil())
+      expr.type()=type;
+  }
+  else if(expr.id()=="constraint_select_one")
+  {
+    typecheck_op(expr, type, mode);
+
+    typet op_type;
+    op_type.make_nil();
+
+    forall_operands(it, expr)
+    {
+      typet tmp;
+      type_union(it->type(), op_type, tmp);
+      op_type=tmp;
+    }
+    
+    Forall_operands(it, expr)
+      typecheck(*it, op_type, mode);
+      
+    expr.type()=op_type;
+  }
+  else if(expr.id()==ID_implies)
+  {
+    if(expr.operands().size()!=2)
+    {
+      err_location(expr);
+      str << "Expected two operands for -> operator";
+      throw 0;
+    }
+
+    typecheck_op(expr, typet(ID_bool), mode);
+  }
+  else if(expr.id()==ID_equal || expr.id()==ID_notequal ||
+          expr.id()==ID_lt || expr.id()==ID_le ||
+          expr.id()==ID_gt || expr.id()==ID_ge)
+  {
+    Forall_operands(it, expr)
+      typecheck(*it, static_cast<const typet &>(get_nil_irep()), mode);
+
+    if(expr.operands().size()!=2)
+    {
+      err_location(expr);
+      str << "Expected two operands for " << expr;
+      throw 0;
+    }
+
+    expr.type()=typet(ID_bool);
+
+    exprt &op0=expr.op0(),
+          &op1=expr.op1();
+          
+    typet op_type;
+
+    type_union(op0.type(), op1.type(), op_type);
+    
+    typecheck(op0, op_type, mode);
+    typecheck(op1, op_type, mode);
+
+    if(expr.id()==ID_lt || expr.id()==ID_le ||
+       expr.id()==ID_gt || expr.id()==ID_ge)
+    {
+      if(op0.type().id()!=ID_range)
+      {
+        err_location(expr);
+        str << "Expected number type for " << to_string(expr);
+        throw 0;
+      }
+    }
+  }
+  else if(expr.id()==ID_plus || expr.id()==ID_minus)
+  {
+    bool minus=expr.id()==ID_minus;
+
+    typecheck_op(expr, type, mode);
+    
+    if(type.is_nil())
+    {
+      if(expr.type().id()==ID_range ||
+         expr.type().id()==ID_bool)
+      {
+        // find proper type for precise arithmetic
+        smv_ranget new_range;
+        bool first=true;
+
+        forall_operands(it, expr)
+        {
+          smv_ranget smv_range;
+          convert_type(it->type(), smv_range);
+
+          if(minus && !first)
+          {
+            smv_range.from.negate();
+            smv_range.to.negate();
+          }
+
+          if(smv_range.to<smv_range.from)
+            std::swap(smv_range.to, smv_range.from);
+
+          new_range.to+=smv_range.to;
+          new_range.from+=smv_range.from;
+
+          if(first) first=false;
+        }
+
+        new_range.to_type(expr.type());
+      }
+    }
+    else if(type.id()!=ID_range)
+    {
+      err_location(expr);
+      str << "Expected number type for "
+          << to_string(expr);
+      throw 0;
+    }
+  }
+  else if(expr.id()==ID_constant)
+  {
+    // already done, but maybe need to change the type
+    if(type.is_not_nil() && type!=expr.type())
+    {
+      mp_integer int_value;
+      bool have_int_value=false;
+      
+      if(expr.type().id()==ID_bool)
+      {
+        int_value=expr.is_true()?1:0;
+        have_int_value=true;
+      }
+      else if(expr.type().id()==ID_range)
+      {
+        int_value=string2integer(id2string(expr.get(ID_value)));
+        have_int_value=true;
+      }
+
+      if(have_int_value)
+      {
+        if(type.id()==ID_bool)
+        {
+          if(int_value==0)
+            expr.make_false();
+          else if(int_value==1)
+            expr.make_true();
+        }
+        else if(type.id()==ID_range)
+        {
+          mp_integer from=string2integer(type.get_string(ID_from)),
+                     to=string2integer(type.get_string(ID_to));
+
+          if(int_value>=from && int_value<=to)
+          {
+            expr=exprt(ID_constant, type);
+            expr.set(ID_value, integer2string(int_value));
+          }
+        }
+      }
+    }
+  }
+  else if(expr.id()=="number_constant")
+  {
+    const std::string &value=expr.get_string(ID_value);
+
+    mp_integer int_value=string2integer(value);
+
+    if(type.is_nil())
+    {
+      expr.type()=typet(ID_range);
+      expr.type().set(ID_from, integer2string(int_value));
+      expr.type().set(ID_to, integer2string(int_value));
+      expr.id(ID_constant);
+    }
+    else
+    {
+      expr.type()=type;
+
+      if(type.id()==ID_bool)
+      {
+        if(int_value==0)
+          expr.make_false();
+        else if(int_value==1)
+          expr.make_true();
+        else
+        {
+          err_location(expr);
+          str << "expected 0 or 1 here, but got " << value;
+          throw 0;
+        }
+      }
+      else if(type.id()==ID_range)
+      {
+        smv_ranget smv_range;
+        convert_type(type, smv_range);
+
+        if(int_value<smv_range.from || int_value>smv_range.to)
+        {
+          err_location(expr);
+          str << "expected " << smv_range.from << ".." << smv_range.to 
+              << " here, but got " << value;
+          throw 0;
+        }
+
+        expr.id(ID_constant);
+      }
+      else
+      {
+        err_location(expr);
+        str << "Unexpected constant: " << value;
+        throw 0;
+      }
+    }
+  }
+  else if(expr.id()==ID_cond)
+  {
+    if(type.is_nil())
+    {
+      bool condition=true;
+      
+      expr.type().make_nil();
+
+      Forall_operands(it, expr)
+      {
+        if(condition)
+          typecheck(*it, typet(ID_bool), mode);
+        else
+        {
+          typecheck(*it, static_cast<const typet &>(get_nil_irep()), mode);
+          type_union(expr.type(), it->type(), expr.type());
+        }
+
+        condition=!condition;
+      }
+    }
+    else
+    {
+      expr.type()=type;
+
+      bool condition=true;
+
+      Forall_operands(it, expr)
+      {
+        if(condition)
+          typecheck(*it, typet(ID_bool), mode);
+        else
+          typecheck(*it, expr.type(), mode);
+
+        condition=!condition;
+      }
+    }
+  } 
+  else if(expr.id()==ID_AG || expr.id()==ID_AX || expr.id()==ID_AF || 
+          expr.id()==ID_EG || expr.id()==ID_EX || expr.id()==ID_EF)
+  {
+    if(expr.operands().size()!=1)
+    {
+      err_location(expr);
+      str << "Expected one operand for " << expr.id_string()
+          << " operator";
+      throw 0;
+    }
+
+    expr.type()=typet(ID_bool);
+
+    typecheck(expr.op0(), expr.type(), mode);
+  }
+  else if(expr.id()==ID_typecast)
+  {
+  }
+  else
+  {
+    err_location(expr);
+    str << "No type checking for " << expr;
+    throw 0;
+  }
+
+  if(!type.is_nil() && expr.type()!=type)
+  {
+    smv_ranget e, t;
+    convert_type(expr.type(), e);
+    convert_type(type, t);
+
+    if(e.is_contained_in(t))
+    {
+      if(e.is_singleton())
+      {
+        if(type.id()==ID_bool)
+        {
+          if(e.from==0)
+            expr.make_false();
+          else
+            expr.make_true();
+        }
+        else
+        {
+          expr=exprt(ID_constant, type);
+          expr.set(ID_value, integer2string(e.from));
+        }
+      }
+      else
+        expr.make_typecast(type);
+
+      return;      
+    }
+
+    err_location(expr);
+    str << "Expected expression of type `" << to_string(type)
+        << "', but got expression `" << to_string(expr)
+        << "', which is of type `" << to_string(expr.type()) << "'";
+    throw 0;
+  }
+}
+
+/*******************************************************************\
+
+Function: smv_typecheckt::convert
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void smv_typecheckt::convert(exprt &expr, expr_modet expr_mode)
+{
+  if(expr.id()=="smv_next")
+  {
+    if(expr_mode!=NORMAL)
+    {
+      err_location(expr);
+      str << "next(next(...)) encountered";
+      throw 0;
+    }
+    
+    assert(expr.operands().size()==1);
+
+    exprt tmp;
+    tmp.swap(expr.op0());
+    expr.swap(tmp);
+
+    convert(expr, NEXT);
+    return;
+  }
+
+  Forall_operands(it, expr)
+    convert(*it, expr_mode);
+
+  if(expr.id()==ID_symbol)
+  {
+    const std::string &identifier=expr.get_string(ID_identifier);
+
+    if(identifier=="TRUE")
+      expr.make_true();
+    else if(identifier=="FALSE")
+      expr.make_false();
+    else if(identifier.find("::")==std::string::npos)
+    {
+      std::string id=module+"::var::"+identifier;
+
+      smv_parse_treet::mc_varst::const_iterator it=
+        modulep->vars.find(identifier);
+
+      if(it!=modulep->vars.end())
+        if(it->second.identifier!="")
+          id=id2string(it->second.identifier);
+
+      expr.set(ID_identifier, id);
+      
+      if(expr_mode==NEXT)
+        expr.id(ID_next_symbol);
+    }
+  }
+  else if(expr.id()=="smv_nondet_choice" ||
+          expr.id()=="smv_union")
+  {
+    if(expr.operands().size()==0)
+    {
+      err_location(expr);
+      str << "expected operand here";
+      throw 0;
+    }
+
+    expr.operands().insert(
+      expr.operands().begin(),
+      static_cast<const exprt &>(get_nil_irep()));
+
+    std::string identifier=
+      module+"::var::"+i2string(nondet_count++);
+
+    expr.op0().clear();
+    expr.op0().id(ID_nondet_symbol);
+    expr.op0().set(ID_identifier, identifier);
+    expr.op0().type().make_nil();
+
+    expr.set("#smv_nondet_choice", true);
+
+    expr.id("constraint_select_one");
+  }
+  else if(expr.id()=="smv_cases") // cases
+  {
+    if(expr.operands().size()<1)
+    {
+      err_location(expr);
+      str << "Expected at least one operand for " << expr.id_string()
+          << " expression";
+      throw 0;
+    }
+
+    exprt tmp;
+    tmp.operands().swap(expr.operands());
+    expr.reserve_operands(tmp.operands().size()*2);
+
+    Forall_operands(it, tmp)
+    {
+      if(it->operands().size()!=2)
+      {
+        err_location(*it);
+        throw "case expected to have two operands";
+      }
+
+      exprt &condition=it->op0();
+      exprt &value=it->op1();
+
+      expr.move_to_operands(condition);
+      expr.move_to_operands(value);
+    }
+
+    expr.id(ID_cond);
+  }
+}
+
+/*******************************************************************\
+
+Function: smv_typecheckt::to_string
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+std::string smv_typecheckt::to_string(const exprt &expr)
+{
+  std::string result;
+  expr2smv(expr, result);
+  return result;
+}
+
+/*******************************************************************\
+
+Function: smv_typecheckt::to_string
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+std::string smv_typecheckt::to_string(const typet &type)
+{
+  std::string result;
+  type2smv(type, result);
+  return result;
+}
+
+/*******************************************************************\
+
+Function: smv_typecheckt::typecheck
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void smv_typecheckt::typecheck(
+  smv_parse_treet::modulet::itemt &item)
+{
+  modet mode;
+
+  switch(item.item_type)
+  {
+  case smv_parse_treet::modulet::itemt::INIT:
+    mode=INIT;
+    break;
+
+  case smv_parse_treet::modulet::itemt::TRANS:
+    mode=TRANS;
+    break;
+
+  default:
+    mode=OTHER;
+  }
+
+  typecheck(item.expr, bool_typet(), mode);
+}
+
+/*******************************************************************\
+
+Function: smv_typecheckt::convert
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void smv_typecheckt::convert(
+  smv_parse_treet::modulet::itemt &item)
+{
+  convert(item.expr, NORMAL);
+}
+
+/*******************************************************************\
+
+Function: smv_typecheckt::convert_vars
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void smv_typecheckt::convert(smv_parse_treet::mc_varst &vars)
+{
+  symbolt symbol;
+
+  symbol.mode="SMV";
+  symbol.module=modulep->name;
+
+  for(smv_parse_treet::mc_varst::const_iterator it=vars.begin();
+      it!=vars.end(); it++)
+  {
+    const smv_parse_treet::mc_vart &var=it->second;
+
+    symbol.base_name=it->first;
+
+    if(var.identifier=="")
+      symbol.name=module+"::var::"+id2string(symbol.base_name);
+    else
+      symbol.name=var.identifier;
+
+    symbol.value.make_nil();
+    symbol.is_input=true;
+    symbol.is_statevar=false;
+    symbol.type=var.type;
+
+    context.add(symbol);
+  }
+}
+
+/*******************************************************************\
+
+Function: smv_typecheckt::collect_define
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void smv_typecheckt::collect_define(const exprt &expr)
+{
+  if(expr.id()!=ID_equal || expr.operands().size()!=2)
+    throw "collect_define expects equality";
+
+  const exprt &op0=expr.op0();
+  const exprt &op1=expr.op1();
+
+  if(op0.id()!=ID_symbol)
+    throw "collect_define expects symbol on left hand side";
+
+  const irep_idt &identifier=op0.get(ID_identifier);
+
+  contextt::symbolst::iterator it=context.symbols.find(identifier);
+
+  if(it==context.symbols.end())
+  {
+    str << "collect_define failed to find symbol `"
+        << identifier << "'";
+    throw 0;
+  }
+
+  symbolt &symbol=it->second;
+
+  symbol.value.make_nil();
+  symbol.is_input=false;
+  symbol.is_statevar=false;
+  symbol.is_macro=false;
+
+  std::pair<define_mapt::iterator, bool> result=
+    define_map.insert(std::pair<irep_idt, definet>(identifier, definet(op1)));
+
+  if(!result.second)
+  {
+    err_location(expr);
+    str << "symbol `" << identifier << "' defined twice" << std::endl;
+    throw 0;
+  }  
+}
+
+/*******************************************************************\
+
+Function: smv_typecheckt::convert_define
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void smv_typecheckt::convert_define(const irep_idt &identifier)
+{
+  definet &d=define_map[identifier];
+  
+  if(d.typechecked) return;
+  
+  if(d.in_progress)
+  {
+    str << "definition of `" << identifier << "' is cyclic";
+    throw 0;
+  }
+  
+  contextt::symbolst::iterator it=context.symbols.find(identifier);
+
+  if(it==context.symbols.end())
+  {
+    str << "convert_define failed to find symbol `"
+        << identifier << "'";
+    throw 0;
+  }
+
+  symbolt &symbol=it->second;
+
+  d.in_progress=true;
+  
+  typecheck(d.value, symbol.type, OTHER);
+  
+  d.in_progress=false;
+  d.typechecked=true;
+
+  if(symbol.type.is_nil())
+    symbol.type=d.value.type();
+}
+
+/*******************************************************************\
+
+Function: smv_typecheckt::convert_defines
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void smv_typecheckt::convert_defines(exprt &invar)
+{
+  for(define_mapt::iterator it=define_map.begin();
+      it!=define_map.end();
+      it++)
+  {
+    convert_define(it->first);
+
+    // generate constraint
+    equal_exprt equality;
+    equality.lhs()=exprt(ID_symbol, it->second.value.type());
+    equality.lhs().set(ID_identifier, it->first);
+    equality.rhs()=it->second.value;
+    invar.move_to_operands(equality);
+  }
+}
+
+/*******************************************************************\
+
+Function: smv_typecheckt::convert
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void smv_typecheckt::convert(smv_parse_treet::modulet &smv_module)
+{
+  modulep=&smv_module;
+
+  define_map.clear();
+
+  convert(smv_module.vars);
+
+  // transition relation
+
+  symbolt module_symbol;
+
+  module_symbol.base_name=smv_module.base_name;
+  module_symbol.pretty_name=smv_module.base_name;
+  module_symbol.name=smv_module.name;
+  module_symbol.module=module_symbol.name;
+  module_symbol.type=typet(ID_module);
+  module_symbol.mode="SMV";
+  module_symbol.value=transt();
+  module_symbol.value.operands().resize(3);
+
+  transt &trans=to_trans_expr(module_symbol.value);
+
+  convert_ports(smv_module, module_symbol.type);
+
+  Forall_item_list(it, smv_module.items)
+    convert(*it);
+
+  flatten_hierarchy(smv_module);
+  
+  // we first need to collect all the defines
+
+  Forall_item_list(it, smv_module.items)
+    if(it->is_define())
+      collect_define(it->expr);
+
+  // now turn them into INVARs
+  convert_defines(trans.invar());
+
+  // do the rest now
+
+  Forall_item_list(it, smv_module.items)
+    if(!it->is_define())
+      typecheck(*it);
+
+  Forall_item_list(it, smv_module.items)
+    if(it->is_invar())
+      trans.invar().move_to_operands(it->expr);
+    else if(it->is_init())
+      trans.init().move_to_operands(it->expr);
+    else if(it->is_trans())
+      trans.trans().move_to_operands(it->expr);
+
+  Forall_operands(it, trans)
+    gen_and(*it);
+
+  context.move(module_symbol);
+
+  // spec
+
+  if(do_spec)
+  {
+    unsigned nr=1;
+
+    forall_item_list(it, smv_module.items)
+      if(it->is_spec())
+      {
+        symbolt spec_symbol;
+
+        spec_symbol.base_name=smv_module.base_name;
+        spec_symbol.name=id2string(smv_module.name)+"::spec"+i2string(nr++);
+        spec_symbol.module=smv_module.name;
+        spec_symbol.type=typet(ID_bool);
+        spec_symbol.theorem=true;
+        spec_symbol.mode="SMV";
+        spec_symbol.value=it->expr;
+        spec_symbol.location=it->location;
+
+        context.move(spec_symbol);
+      }
+  }
+}
+
+/*******************************************************************\
+
+Function: smv_typecheckt::typecheck
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void smv_typecheckt::typecheck()
+{
+  smv_parse_treet::modulest::iterator it=smv_parse_tree.modules.find(module);
+
+  if(it==smv_parse_tree.modules.end())
+  {
+    str << "failed to find module " << module;
+    throw 0;
+  }
+
+  convert(it->second);
+}
+
+/*******************************************************************\
+
+Function: smv_typecheck
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+bool smv_typecheck(
+  smv_parse_treet &smv_parse_tree,
+  contextt &context,
+  const std::string &module,
+  message_handlert &message_handler,
+  bool do_spec)
+{
+  smv_typecheckt smv_typecheck(
+    smv_parse_tree, context, module, do_spec, message_handler);
+  return smv_typecheck.typecheck_main();
+}
+
+/*******************************************************************\
+
+Function: smv_module_symbol
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+std::string smv_module_symbol(const std::string &module)
+{
+  return "smv::"+module;
+}
diff --git a/src/ebmc/smvlang/smv_typecheck.d b/src/ebmc/smvlang/smv_typecheck.d
new file mode 100644
index 0000000..013cfaf
--- /dev/null
+++ b/src/ebmc/smvlang/smv_typecheck.d
@@ -0,0 +1,10 @@
+smv_typecheck.o: smv_typecheck.cpp ../util/expr_util.h ../util/irep.h \
+  ../util/dstring.h ../util/string_container.h ../util/hash_cont.h \
+  ../util/string_hash.h ../util/irep_ids.h ../util/location.h \
+  ../util/typecheck.h ../util/message_stream.h ../util/message.h \
+  ../util/location.h ../util/expr.h ../util/type.h ../util/arith_tools.h \
+  ../util/mp_arith.h ../big-int/bigint.hh ../util/i2string.h \
+  ../util/std_expr.h ../util/std_types.h ../util/expr.h \
+  ../util/mp_arith.h smv_typecheck.h ../util/context.h \
+  ../util/hash_cont.h ../util/symbol.h ../util/message.h smv_parse_tree.h \
+  ../util/string_hash.h expr2smv.h
diff --git a/src/ebmc/smvlang/smv_typecheck.h b/src/ebmc/smvlang/smv_typecheck.h
new file mode 100644
index 0000000..9212ca7
--- /dev/null
+++ b/src/ebmc/smvlang/smv_typecheck.h
@@ -0,0 +1,26 @@
+/*******************************************************************\
+
+Module: SMV Typechecking
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#ifndef CPROVER_SMV_TYPECHECK_H
+#define CPROVER_SMV_TYPECHECK_H
+
+#include <context.h>
+#include <message.h>
+
+#include "smv_parse_tree.h"
+
+bool smv_typecheck(
+  smv_parse_treet &smv_parse_tree,
+  contextt &context,
+  const std::string &module,
+  message_handlert &message_handler,
+  bool do_spec=true);
+
+std::string smv_module_symbol(const std::string &module);
+
+#endif