diff --git a/CHANGELOG b/CHANGELOG
index 0dc09ce68..f140186d0 100644
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -4,6 +4,7 @@
 * SystemVerilog: assignment patterns with keys for structs
 * SMV: LTL V operator, xnor operator
 * SMV: word types and operators
+* --smv-word-level outputs the model as word-level SMV
 
 # EBMC 5.5
 
diff --git a/regression/ebmc/smv-word-level/verilog1.desc b/regression/ebmc/smv-word-level/verilog1.desc
new file mode 100644
index 000000000..e8af1cfaf
--- /dev/null
+++ b/regression/ebmc/smv-word-level/verilog1.desc
@@ -0,0 +1,11 @@
+CORE
+verilog1.v
+--smv-word-level
+^MODULE main$
+^VAR x : unsigned word\[32\];$
+^INIT main\.x = 0ud32_0$
+^INVAR Verilog::main\.x_aux0 = main\.x \+ 0ud32_1$
+^TRANS next\(main\.x\) = Verilog::main\.x_aux0$
+^EXIT=0$
+^SIGNAL=0$
+--
diff --git a/regression/ebmc/smv-word-level/verilog1.v b/regression/ebmc/smv-word-level/verilog1.v
new file mode 100644
index 000000000..77eaaad01
--- /dev/null
+++ b/regression/ebmc/smv-word-level/verilog1.v
@@ -0,0 +1,10 @@
+module main(input clk);
+
+  reg [31:0] x;
+
+  initial x = 0;
+
+  always @(posedge clk)
+    x = x + 1;
+
+endmodule
diff --git a/src/ebmc/Makefile b/src/ebmc/Makefile
index be0fd58e0..da61dc177 100644
--- a/src/ebmc/Makefile
+++ b/src/ebmc/Makefile
@@ -24,6 +24,7 @@ SRC = \
       netlist.cpp \
       neural_liveness.cpp \
       output_file.cpp \
+      output_smv_word_level.cpp \
       output_verilog.cpp \
       property_checker.cpp \
       random_traces.cpp \
diff --git a/src/ebmc/ebmc_parse_options.cpp b/src/ebmc/ebmc_parse_options.cpp
index f9189eddb..18fa0775d 100644
--- a/src/ebmc/ebmc_parse_options.cpp
+++ b/src/ebmc/ebmc_parse_options.cpp
@@ -21,6 +21,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "netlist.h"
 #include "neural_liveness.h"
 #include "output_file.h"
+#include "output_smv_word_level.h"
 #include "property_checker.h"
 #include "random_traces.h"
 #include "ranking_function.h"
@@ -215,6 +216,15 @@ int ebmc_parse_optionst::doit()
     auto properties = ebmc_propertiest::from_command_line(
       cmdline, transition_system, ui_message_handler);
 
+    if(cmdline.isset("smv-word-level"))
+    {
+      auto filename = cmdline.value_opt("outfile").value_or("-");
+      output_filet output_file{filename};
+      output_smv_word_level(
+        transition_system, properties, output_file.stream());
+      return 0;
+    }
+
     if(cmdline.isset("show-properties"))
     {
       show_properties(properties, ui_message_handler);
@@ -418,6 +428,7 @@ void ebmc_parse_optionst::help()
     " {y--smv-netlist}               \t show netlist in SMV format\n"
     " {y--dot-netlist}               \t show netlist in DOT format\n"
     " {y--show-trans}                \t show transition system\n"
+    " {y--smv-word-level}            \t output word-level SMV\n"
     " {y--verbosity} {u#}            \t verbosity level, from 0 (silent) to 10 (everything)\n"
     // clang-format on
     "\n");
diff --git a/src/ebmc/ebmc_parse_options.h b/src/ebmc/ebmc_parse_options.h
index 03bb8772b..aa3b69688 100644
--- a/src/ebmc/ebmc_parse_options.h
+++ b/src/ebmc/ebmc_parse_options.h
@@ -44,7 +44,8 @@ class ebmc_parse_optionst:public parse_options_baset
         "(smt2)(bitwuzla)(boolector)(cvc3)(cvc4)(cvc5)(mathsat)(yices)(z3)"
         "(minisat)(cadical)"
         "(aig)(stop-induction)(stop-minimize)(start):(coverage)(naive)"
-        "(compute-ct)(dot-netlist)(smv-netlist)(vcd):"
+        "(compute-ct)(dot-netlist)(smv-netlist)(smv-word-level)"
+        "(vcd):"
         "(random-traces)(trace-steps):(random-seed):(traces):"
         "(random-trace)(random-waveform)"
         "(bmc-with-assumptions)"
diff --git a/src/ebmc/output_smv_word_level.cpp b/src/ebmc/output_smv_word_level.cpp
new file mode 100644
index 000000000..ac8837eff
--- /dev/null
+++ b/src/ebmc/output_smv_word_level.cpp
@@ -0,0 +1,217 @@
+/*******************************************************************\
+
+Module: Word-Level SMV Output
+
+Author: Daniel Kroening, dkr@amazon.com
+
+\*******************************************************************/
+
+#include "output_smv_word_level.h"
+
+#include <util/bitvector_types.h>
+
+#include <smvlang/expr2smv.h>
+
+#include "ebmc_error.h"
+#include "ebmc_properties.h"
+#include "transition_system.h"
+
+#include <ostream>
+
+class smv_type_printert
+{
+public:
+  explicit smv_type_printert(const typet &__type) : _type(__type)
+  {
+  }
+
+  const typet &type() const
+  {
+    return _type;
+  }
+
+protected:
+  const typet &_type;
+};
+
+std::ostream &
+operator<<(std::ostream &out, const smv_type_printert &type_printer)
+{
+  auto &type = type_printer.type();
+
+  if(type.id() == ID_bool)
+    return out << "boolean";
+  else if(type.id() == ID_signedbv)
+    return out << "signed word[" << to_signedbv_type(type).get_width() << "]";
+  else if(type.id() == ID_unsignedbv)
+    return out << "unsigned word[" << to_unsignedbv_type(type).get_width()
+               << "]";
+  else
+    throw ebmc_errort{} << "cannot convert type " << type.id() << " to SMV";
+
+  return out;
+}
+
+static void smv_state_variables(
+  const transition_systemt &transition_system,
+  std::ostream &out)
+{
+  bool found = false;
+
+  const auto module = transition_system.main_symbol->name;
+  const auto &symbol_table = transition_system.symbol_table;
+
+  for(auto m_it = symbol_table.symbol_module_map.lower_bound(module);
+      m_it != symbol_table.symbol_module_map.upper_bound(module);
+      m_it++)
+  {
+    const irep_idt &identifier = m_it->second;
+
+    symbol_tablet::symbolst::const_iterator s_it =
+      symbol_table.symbols.find(identifier);
+
+    if(s_it == symbol_table.symbols.end())
+      throw ebmc_errort{} << "failed to find symbol " << identifier;
+
+    const symbolt &symbol = s_it->second;
+
+    if(symbol.is_state_var)
+    {
+      out << "VAR " << symbol.base_name << " : "
+          << smv_type_printert{symbol.type} << ";\n";
+      found = true;
+    }
+  }
+
+  if(found)
+    out << '\n';
+}
+
+static void
+smv_initial_states(const exprt &expr, const namespacet &ns, std::ostream &out)
+{
+  if(expr.id() == ID_and)
+  {
+    for(auto &conjunct : expr.operands())
+      smv_initial_states(conjunct, ns, out);
+  }
+  else if(expr.is_true())
+  {
+    // ignore
+  }
+  else
+  {
+    out << "INIT " << expr2smv(expr, ns) << '\n';
+  }
+}
+
+static void smv_initial_states(
+  const transition_systemt &transition_system,
+  std::ostream &out)
+{
+  const namespacet ns(transition_system.symbol_table);
+  smv_initial_states(transition_system.trans_expr.init(), ns, out);
+}
+
+static void
+smv_invar(const exprt &expr, const namespacet &ns, std::ostream &out)
+{
+  if(expr.id() == ID_and)
+  {
+    for(auto &conjunct : expr.operands())
+      smv_initial_states(conjunct, ns, out);
+  }
+  else if(expr.is_true())
+  {
+    // ignore
+  }
+  else
+  {
+    out << "INVAR " << expr2smv(expr, ns) << '\n';
+  }
+}
+
+static void
+smv_invar(const transition_systemt &transition_system, std::ostream &out)
+{
+  const namespacet ns(transition_system.symbol_table);
+  smv_invar(transition_system.trans_expr.invar(), ns, out);
+}
+
+static void smv_transition_relation(
+  const exprt &expr,
+  const namespacet &ns,
+  std::ostream &out)
+{
+  if(expr.id() == ID_and)
+  {
+    for(auto &conjunct : expr.operands())
+      smv_initial_states(conjunct, ns, out);
+  }
+  else if(expr.is_true())
+  {
+    // ignore
+  }
+  else
+  {
+    out << "TRANS " << expr2smv(expr, ns) << '\n';
+  }
+}
+
+static void smv_transition_relation(
+  const transition_systemt &transition_system,
+  std::ostream &out)
+{
+  const namespacet ns(transition_system.symbol_table);
+  smv_transition_relation(transition_system.trans_expr.trans(), ns, out);
+}
+
+static void smv_properties(
+  const transition_systemt &transition_system,
+  const ebmc_propertiest &properties,
+  std::ostream &out)
+{
+  const namespacet ns(transition_system.symbol_table);
+
+  for(auto &property : properties.properties)
+  {
+    if(property.is_disabled() || property.is_assumed())
+      continue;
+
+    if(is_CTL(property.normalized_expr))
+    {
+      out << "CTLSPEC " << expr2smv(property.normalized_expr, ns);
+    }
+    else if(is_LTL(property.normalized_expr))
+    {
+      out << "LTLSPEC " << expr2smv(property.normalized_expr, ns);
+    }
+    else
+      out << "-- " << property.identifier << ": not converted\n";
+
+    out << '\n';
+  }
+}
+
+void output_smv_word_level(
+  const transition_systemt &transition_system,
+  const ebmc_propertiest &properties,
+  std::ostream &out)
+{
+  out << "MODULE main\n\n";
+
+  // state-holding elements first
+  smv_state_variables(transition_system, out);
+
+  // initial state constraints
+  smv_initial_states(transition_system, out);
+
+  // in-state invariants
+  smv_invar(transition_system, out);
+
+  // transition relation
+  smv_transition_relation(transition_system, out);
+
+  // properties
+  smv_properties(transition_system, properties, out);
+}
diff --git a/src/ebmc/output_smv_word_level.h b/src/ebmc/output_smv_word_level.h
new file mode 100644
index 000000000..62372ae0b
--- /dev/null
+++ b/src/ebmc/output_smv_word_level.h
@@ -0,0 +1,23 @@
+/*******************************************************************\
+
+Module: Word-Level SMV Output
+
+Author: Daniel Kroening, dkr@amazon.com
+
+\*******************************************************************/
+
+#ifndef EBMC_OUTPUT_SMV_WORD_LEVEL_H
+#define EBMC_OUTPUT_SMV_WORD_LEVEL_H
+
+#include <iosfwd>
+
+class ebmc_propertiest;
+class transition_systemt;
+
+/// outputs word-level SMV
+void output_smv_word_level(
+  const transition_systemt &,
+  const ebmc_propertiest &,
+  std::ostream &);
+
+#endif // EBMC_OUTPUT_SMV_WORD_LEVEL_H
diff --git a/src/smvlang/expr2smv.cpp b/src/smvlang/expr2smv.cpp
index a41642fbf..236098e9e 100644
--- a/src/smvlang/expr2smv.cpp
+++ b/src/smvlang/expr2smv.cpp
@@ -103,7 +103,9 @@ class expr2smvt
 
   bool convert_if(const if_exprt &, std::string &dest, precedencet precedence);
 
-  bool convert(const exprt &src, std::string &dest);
+  std::string convert(const exprt &);
+
+  bool convert(const exprt &, std::string &dest);
 
   bool convert_symbol(
     const symbol_exprt &,
@@ -125,8 +127,6 @@ class expr2smvt
   bool
   convert_norep(const exprt &src, std::string &dest, precedencet &precedence);
 
-  bool convert(const typet &src, std::string &dest);
-
 protected:
   const namespacet &ns;
 };
@@ -790,6 +790,25 @@ Function: expr2smvt::convert
 
 \*******************************************************************/
 
+std::string expr2smvt::convert(const exprt &src)
+{
+  std::string dest;
+  convert(src, dest);
+  return dest;
+}
+
+/*******************************************************************\
+
+Function: expr2smvt::convert
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
 bool expr2smvt::convert(const exprt &src, std::string &dest)
 {
   precedencet precedence;
@@ -808,10 +827,10 @@ Function: expr2smv
 
 \*******************************************************************/
 
-bool expr2smv(const exprt &expr, std::string &code, const namespacet &ns)
+std::string expr2smv(const exprt &expr, const namespacet &ns)
 {
-  expr2smvt expr2smv(ns);
-  return expr2smv.convert(expr, code);
+  expr2smvt expr2smv{ns};
+  return expr2smv.convert(expr);
 }
 
 /*******************************************************************\
@@ -826,24 +845,22 @@ Function: type2smv
 
 \*******************************************************************/
 
-bool type2smv(const typet &type, std::string &code, const namespacet &ns)
+std::string type2smv(const typet &type, const namespacet &ns)
 {
   if(type.id()==ID_bool)
-    code="boolean";
+    return "boolean";
   else if(type.id()==ID_array)
   {
-    std::string tmp;
-    if(type2smv(to_array_type(type).element_type(), tmp, ns))
-      return true;
-    code="array ";
+    std::string code = "array ";
     code+="..";
     code+=" of ";
-    code+=tmp;
+    code += type2smv(to_array_type(type).element_type(), ns);
+    return code;
   }
   else if(type.id()==ID_enumeration)
   {
     const irept::subt &elements=to_enumeration_type(type).elements();
-    code="{ ";
+    std::string code = "{ ";
     bool first=true;
     for(auto &element : elements)
     {
@@ -851,14 +868,15 @@ bool type2smv(const typet &type, std::string &code, const namespacet &ns)
       code += element.id_string();
     }
     code+=" }";
+    return code;
   }
   else if(type.id()==ID_range)
   {
-    code=type.get_string(ID_from)+".."+type.get_string(ID_to);
+    return type.get_string(ID_from) + ".." + type.get_string(ID_to);
   }
   else if(type.id()=="submodule")
   {
-    code=type.get_string(ID_identifier);
+    auto code = type.get_string(ID_identifier);
     const exprt &e=(exprt &)type;
     if(e.has_operands())
     {
@@ -867,25 +885,22 @@ bool type2smv(const typet &type, std::string &code, const namespacet &ns)
       forall_operands(it, e)
       {
         if(first) first=false; else code+=", ";
-        std::string tmp;
-        expr2smv(*it, tmp, ns);
-        code+=tmp;
+        code += expr2smv(*it, ns);
       }
       code+=')';
     }
+    return code;
   }
   else if(type.id() == ID_signedbv)
   {
-    code =
-      "signed word[" + std::to_string(to_signedbv_type(type).width()) + ']';
+    return "signed word[" + std::to_string(to_signedbv_type(type).width()) +
+           ']';
   }
   else if(type.id() == ID_unsignedbv)
   {
-    code =
-      "unsigned word[" + std::to_string(to_unsignedbv_type(type).width()) + ']';
+    return "unsigned word[" + std::to_string(to_unsignedbv_type(type).width()) +
+           ']';
   }
   else
-    return true;
-
-  return false;
+    return "no conversion for " + type.id_string();
 }
diff --git a/src/smvlang/expr2smv.h b/src/smvlang/expr2smv.h
index 16a76b7eb..3e57c8d2b 100644
--- a/src/smvlang/expr2smv.h
+++ b/src/smvlang/expr2smv.h
@@ -8,5 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/expr.h>
 
-bool expr2smv(const exprt &, std::string &code, const namespacet &);
-bool type2smv(const typet &, std::string &code, const namespacet &);
+class namespacet;
+
+std::string expr2smv(const exprt &, const namespacet &);
+std::string type2smv(const typet &, const namespacet &);
diff --git a/src/smvlang/smv_language.cpp b/src/smvlang/smv_language.cpp
index 4b04e86bd..c401449dd 100644
--- a/src/smvlang/smv_language.cpp
+++ b/src/smvlang/smv_language.cpp
@@ -140,12 +140,10 @@ void smv_languaget::show_parse(std::ostream &out, message_handlert &)
         it!=module.vars.end(); it++)
       if(it->second.type.id()!="submodule")
       {
-        std::string msg;
         symbol_tablet symbol_table;
-        namespacet ns(symbol_table);
-        type2smv(it->second.type, msg, ns);
-        out << "    " << it->first << ": " 
-            << msg << ";" << std::endl;
+        namespacet ns{symbol_table};
+        auto msg = type2smv(it->second.type, ns);
+        out << "    " << it->first << ": " << msg << ";\n";
       }
 
     out << std::endl;
@@ -157,12 +155,10 @@ void smv_languaget::show_parse(std::ostream &out, message_handlert &)
         it!=module.vars.end(); it++)
       if(it->second.type.id()=="submodule")
       {
-        std::string msg;
         symbol_tablet symbol_table;
         namespacet ns(symbol_table);
-        type2smv(it->second.type, msg, ns);
-        out << "    " << it->first << ": " 
-            << msg << ";" << std::endl;
+        auto msg = type2smv(it->second.type, ns);
+        out << "    " << it->first << ": " << msg << ";\n";
       }
 
     out << std::endl;
@@ -193,7 +189,8 @@ Function: smv_languaget::from_expr
 bool smv_languaget::from_expr(const exprt &expr, std::string &code,
                               const namespacet &ns)
 {
-  return expr2smv(expr, code, ns);
+  code = expr2smv(expr, ns);
+  return false;
 }
 
 /*******************************************************************\
@@ -213,7 +210,8 @@ bool smv_languaget::from_type(
   std::string &code,
   const namespacet &ns)
 {
-  return type2smv(type, code, ns);
+  code = type2smv(type, ns);
+  return false;
 }
 
 /*******************************************************************\
diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp
index c1ed26f3a..16cab011d 100644
--- a/src/smvlang/smv_typecheck.cpp
+++ b/src/smvlang/smv_typecheck.cpp
@@ -1529,10 +1529,8 @@ Function: smv_typecheckt::to_string
 
 std::string smv_typecheckt::to_string(const exprt &expr)
 {
-  std::string result;
-  namespacet ns(symbol_table);
-  expr2smv(expr, result, ns);
-  return result;
+  namespacet ns{symbol_table};
+  return expr2smv(expr, ns);
 }
 
 /*******************************************************************\
@@ -1549,10 +1547,8 @@ Function: smv_typecheckt::to_string
 
 std::string smv_typecheckt::to_string(const typet &type)
 {
-  std::string result;
-  namespacet ns(symbol_table);
-  type2smv(type, result, ns);
-  return result;
+  namespacet ns{symbol_table};
+  return type2smv(type, ns);
 }
 
 /*******************************************************************\