diff --git a/doc/vs-cmurphi.rst b/doc/vs-cmurphi.rst
index 99c037b4..39896992 100644
--- a/doc/vs-cmurphi.rst
+++ b/doc/vs-cmurphi.rst
@@ -37,7 +37,25 @@ Type System
 -----------
 CMurphi supports real arithmetic using the ``real`` data type. Rumur does not
 support this type and there are no plans to implement this or any floating point
-support. Similarly, Rumur does not support the ``union`` or ``multiset`` types.
+support. Similarly, Rumur does not support the ``multiset`` type.
+
+Unions
+^^^^^^
+Models that use the ``union`` type can be parsed with librumur, but generation
+of a checker using ``rumur`` is not supported. Some of the Rumur tools fully
+support union types, e.g. ``murphi2xml``, but others reject models with union
+types, e.g. ``murphi2uclid``.
+
+CMurphi only supports unions of scalarset and enum types. librumur supports
+unions of any types, simple or complex, including recursive (unions of unions).
+In contrast to CMurphi, librumur allows union types with 0 or 1 members. A union
+type with 0 members is vacuous, in the sense that values of this type can only
+ever be ``undefined``.
+
+CMurphi requires the first argument to the ``ismember`` predicate to be a
+designator. librumur allows any expression. CMurphi requires the second argument
+to ``ismember`` to be a scalarset or enum type. librumur, in line with
+supporting unions of any types, allows the second argument to be any type.
 
 Assumptions
 -----------
diff --git a/librumur/include/rumur/Expr.h b/librumur/include/rumur/Expr.h
index 7e32e639..88e86350 100644
--- a/librumur/include/rumur/Expr.h
+++ b/librumur/include/rumur/Expr.h
@@ -676,6 +676,25 @@ struct RUMUR_API_WITH_RTTI Forall : public Expr {
   bool is_pure() const override;
 };
 
+struct RUMUR_API_WITH_RTTI IsMember : public Expr {
+
+  Ptr<Expr> peg;
+  Ptr<TypeExpr> hole;
+
+  IsMember(const Ptr<Expr> &peg_, const Ptr<TypeExpr> &hole_,
+           const location &loc_);
+  IsMember *clone() const override;
+
+  void visit(BaseTraversal &visitor) override;
+  void visit(ConstBaseTraversal &visitor) const override;
+
+  bool constant() const override;
+  Ptr<TypeExpr> type() const override;
+  mpz_class constant_fold() const override;
+  void to_stream(std::ostream &out) const override;
+  bool is_pure() const override;
+};
+
 struct RUMUR_API_WITH_RTTI IsUndefined : public UnaryExpr {
 
   IsUndefined(const Ptr<Expr> &expr_, const location &loc_);
diff --git a/librumur/include/rumur/TypeExpr.h b/librumur/include/rumur/TypeExpr.h
index a8592490..0adb8ae1 100644
--- a/librumur/include/rumur/TypeExpr.h
+++ b/librumur/include/rumur/TypeExpr.h
@@ -190,4 +190,22 @@ struct RUMUR_API_WITH_RTTI TypeExprID : public TypeExpr {
   bool constant() const override;
 };
 
+struct RUMUR_API_WITH_RTTI Union : public TypeExpr {
+  std::vector<Ptr<TypeExpr>> members;
+
+  Union(const std::vector<Ptr<TypeExpr>> &members_, const location &loc_);
+  Union *clone() const override;
+
+  void visit(BaseTraversal &visitor) override;
+  void visit(ConstBaseTraversal &visitor) const override;
+
+  mpz_class count() const override;
+  bool is_simple() const override;
+  void validate() const override;
+  mpz_class lower_bound() const override;
+  mpz_class upper_bound() const override;
+  void to_stream(std::ostream &out) const override;
+  bool constant() const override;
+};
+
 } // namespace rumur
diff --git a/librumur/include/rumur/indexer.h b/librumur/include/rumur/indexer.h
index 16cccb4a..5aac00bc 100644
--- a/librumur/include/rumur/indexer.h
+++ b/librumur/include/rumur/indexer.h
@@ -52,6 +52,7 @@ class RUMUR_API_WITH_RTTI Indexer : public BaseTraversal {
   void visit_if(If &n) override;
   void visit_ifclause(IfClause &n) override;
   void visit_implication(Implication &n) override;
+  void visit_ismember(IsMember &n) override;
   void visit_isundefined(IsUndefined &n) override;
   void visit_leq(Leq &n) override;
   void visit_lsh(Lsh &n) override;
@@ -85,6 +86,7 @@ class RUMUR_API_WITH_RTTI Indexer : public BaseTraversal {
   void visit_typedecl(TypeDecl &n) override;
   void visit_typeexprid(TypeExprID &n) override;
   void visit_undefine(Undefine &n) override;
+  void visit_union(Union &n) override;
   void visit_vardecl(VarDecl &n) override;
   void visit_while(While &n) override;
   void visit_xor(Xor &n) override;
diff --git a/librumur/include/rumur/traverse.h b/librumur/include/rumur/traverse.h
index 60d4bf56..c92bd0e8 100644
--- a/librumur/include/rumur/traverse.h
+++ b/librumur/include/rumur/traverse.h
@@ -98,6 +98,7 @@ class RUMUR_API_WITH_RTTI BaseTraversal {
   virtual void visit_if(If &n) = 0;
   virtual void visit_ifclause(IfClause &n) = 0;
   virtual void visit_implication(Implication &n) = 0;
+  virtual void visit_ismember(IsMember &n) = 0;
   virtual void visit_isundefined(IsUndefined &n) = 0;
   virtual void visit_leq(Leq &n) = 0;
   virtual void visit_lsh(Lsh &n) = 0;
@@ -131,6 +132,7 @@ class RUMUR_API_WITH_RTTI BaseTraversal {
   virtual void visit_typedecl(TypeDecl &n) = 0;
   virtual void visit_typeexprid(TypeExprID &n) = 0;
   virtual void visit_undefine(Undefine &n) = 0;
+  virtual void visit_union(Union &n) = 0;
   virtual void visit_vardecl(VarDecl &n) = 0;
   virtual void visit_while(While &n) = 0;
   virtual void visit_xor(Xor &n) = 0;
@@ -184,6 +186,7 @@ class RUMUR_API_WITH_RTTI Traversal : public BaseTraversal {
   void visit_if(If &n) override;
   void visit_ifclause(IfClause &n) override;
   void visit_implication(Implication &n) override;
+  void visit_ismember(IsMember &n) override;
   void visit_isundefined(IsUndefined &n) override;
   void visit_leq(Leq &n) override;
   void visit_lsh(Lsh &n) override;
@@ -217,6 +220,7 @@ class RUMUR_API_WITH_RTTI Traversal : public BaseTraversal {
   void visit_typedecl(TypeDecl &n) override;
   void visit_typeexprid(TypeExprID &n) override;
   void visit_undefine(Undefine &n) override;
+  void visit_union(Union &n) override;
   void visit_vardecl(VarDecl &n) override;
   void visit_while(While &n) override;
   void visit_xor(Xor &n) override;
@@ -262,6 +266,7 @@ class RUMUR_API_WITH_RTTI ConstBaseTraversal {
   virtual void visit_if(const If &n) = 0;
   virtual void visit_ifclause(const IfClause &n) = 0;
   virtual void visit_implication(const Implication &n) = 0;
+  virtual void visit_ismember(const IsMember &n) = 0;
   virtual void visit_isundefined(const IsUndefined &n) = 0;
   virtual void visit_leq(const Leq &n) = 0;
   virtual void visit_lsh(const Lsh &n) = 0;
@@ -295,6 +300,7 @@ class RUMUR_API_WITH_RTTI ConstBaseTraversal {
   virtual void visit_typedecl(const TypeDecl &n) = 0;
   virtual void visit_typeexprid(const TypeExprID &n) = 0;
   virtual void visit_undefine(const Undefine &n) = 0;
+  virtual void visit_union(const Union &n) = 0;
   virtual void visit_vardecl(const VarDecl &n) = 0;
   virtual void visit_while(const While &n) = 0;
   virtual void visit_xor(const Xor &n) = 0;
@@ -340,6 +346,7 @@ class RUMUR_API_WITH_RTTI ConstTraversal : public ConstBaseTraversal {
   void visit_if(const If &n) override;
   void visit_ifclause(const IfClause &n) override;
   void visit_implication(const Implication &n) override;
+  void visit_ismember(const IsMember &n) override;
   void visit_isundefined(const IsUndefined &n) override;
   void visit_leq(const Leq &n) override;
   void visit_lsh(const Lsh &n) override;
@@ -373,6 +380,7 @@ class RUMUR_API_WITH_RTTI ConstTraversal : public ConstBaseTraversal {
   void visit_typedecl(const TypeDecl &n) override;
   void visit_typeexprid(const TypeExprID &n) override;
   void visit_undefine(const Undefine &n) override;
+  void visit_union(const Union &n) override;
   void visit_vardecl(const VarDecl &n) override;
   void visit_while(const While &n) override;
   void visit_xor(const Xor &n) override;
@@ -424,6 +432,7 @@ class RUMUR_API_WITH_RTTI ConstExprTraversal : public ConstBaseTraversal {
   void visit_typedecl(const TypeDecl &n) final;
   void visit_typeexprid(const TypeExprID &n) final;
   void visit_undefine(const Undefine &n) final;
+  void visit_union(const Union &n) final;
   void visit_vardecl(const VarDecl &n) final;
   void visit_while(const While &n) final;
 };
@@ -458,6 +467,7 @@ class RUMUR_API_WITH_RTTI ConstStmtTraversal : public ConstBaseTraversal {
   void visit_gt(const Gt &n) final;
   void visit_ifclause(const IfClause &n) final;
   void visit_implication(const Implication &n) final;
+  void visit_ismember(const IsMember &n) final;
   void visit_isundefined(const IsUndefined &n) final;
   void visit_leq(const Leq &n) final;
   void visit_lsh(const Lsh &n) final;
@@ -485,6 +495,7 @@ class RUMUR_API_WITH_RTTI ConstStmtTraversal : public ConstBaseTraversal {
   void visit_ternary(const Ternary &n) final;
   void visit_typedecl(const TypeDecl &n) final;
   void visit_typeexprid(const TypeExprID &n) final;
+  void visit_union(const Union &n) final;
   void visit_vardecl(const VarDecl &n) final;
   void visit_xor(const Xor &n) final;
 
@@ -524,6 +535,7 @@ class RUMUR_API_WITH_RTTI ConstTypeTraversal : public ConstBaseTraversal {
   void visit_if(const If &n) final;
   void visit_ifclause(const IfClause &n) final;
   void visit_implication(const Implication &n) final;
+  void visit_ismember(const IsMember &n) final;
   void visit_isundefined(const IsUndefined &n) final;
   void visit_leq(const Leq &n) final;
   void visit_lsh(const Lsh &n) final;
diff --git a/librumur/src/Expr.cc b/librumur/src/Expr.cc
index 32f65580..82a2e02a 100644
--- a/librumur/src/Expr.cc
+++ b/librumur/src/Expr.cc
@@ -1398,8 +1398,10 @@ void FunctionCall::validate() const {
     // callee’s handles are compatible
     if (!v->is_readonly() && isa<Range>(param_type)) {
       const Ptr<TypeExpr> arg_type = a_type->resolve();
-      assert(isa<Range>(arg_type) &&
-             "non-range considered type-compatible with range");
+      if (!isa<Range>(arg_type))
+        throw Error("non-range typed function call argument passed as "
+                    "range-typed var parameter",
+                    (*it)->loc);
 
       auto p = dynamic_cast<const Range &>(*param_type);
       auto a = dynamic_cast<const Range &>(*arg_type);
@@ -1672,6 +1674,34 @@ void Forall::to_stream(std::ostream &out) const {
 
 bool Forall::is_pure() const { return quantifier.is_pure() && expr->is_pure(); }
 
+IsMember::IsMember(const Ptr<Expr> &peg_, const Ptr<TypeExpr> &hole_,
+                   const location &loc_)
+    : Expr(loc_), peg(peg_), hole(hole_) {}
+
+IsMember *IsMember::clone() const { return new IsMember(*this); }
+
+void IsMember::visit(BaseTraversal &visitor) {
+  return visitor.visit_ismember(*this);
+}
+
+void IsMember::visit(ConstBaseTraversal &visitor) const {
+  return visitor.visit_ismember(*this);
+}
+
+bool IsMember::constant() const { return false; }
+
+Ptr<TypeExpr> IsMember::type() const { return Boolean; }
+
+mpz_class IsMember::constant_fold() const {
+  throw Error("ismember used in constant", loc);
+}
+
+void IsMember::to_stream(std::ostream &out) const {
+  out << "ismember(" << *peg << ", " << *hole << ')';
+}
+
+bool IsMember::is_pure() const { return peg->is_pure(); }
+
 IsUndefined::IsUndefined(const Ptr<Expr> &expr_, const location &loc_)
     : UnaryExpr(expr_, loc_) {}
 
diff --git a/librumur/src/TypeExpr.cc b/librumur/src/TypeExpr.cc
index 680531f2..1e0c75b5 100644
--- a/librumur/src/TypeExpr.cc
+++ b/librumur/src/TypeExpr.cc
@@ -147,6 +147,19 @@ static bool equal(const TypeExpr &t1, const TypeExpr &t2) {
     }
 
     void visit_typeexprid(const TypeExprID &n) final { dispatch(*n.referent); }
+
+    void visit_union(const Union &n) final {
+      if (auto u = dynamic_cast<const Union *>(t.get())) {
+        if (u->members.size() != n.members.size()) {
+          result = false;
+        } else {
+          for (size_t i = 0; i < n.members.size(); ++i)
+            result &= equal(*u->members[i], *n.members[i]);
+        }
+      } else {
+        result = false;
+      }
+    }
   };
 
   Equater eq(t1);
@@ -162,6 +175,22 @@ bool TypeExpr::coerces_to(const TypeExpr &other) const {
   if (isa<Range>(t1) && isa<Range>(t2))
     return true;
 
+  if (auto u = dynamic_cast<const Union *>(t2.get())) {
+    for (const Ptr<TypeExpr> &m : u->members) {
+      if (t1->coerces_to(*m))
+        return true;
+    }
+    return false;
+  }
+
+  if (auto u = dynamic_cast<const Union *>(t1.get())) {
+    for (const Ptr<TypeExpr> &m : u->members) {
+      if (m->coerces_to(*t2))
+        return true;
+    }
+    return false;
+  }
+
   return equal(*t1, *t2);
 }
 
@@ -477,4 +506,99 @@ bool TypeExprID::constant() const {
   return referent->value->constant();
 }
 
+Union::Union(const std::vector<Ptr<TypeExpr>> &members_, const location &loc_)
+    : TypeExpr(loc_), members(members_) {}
+
+Union *Union::clone() const { return new Union(*this); }
+
+void Union::visit(BaseTraversal &visitor) { visitor.visit_union(*this); }
+
+void Union::visit(ConstBaseTraversal &visitor) const {
+  visitor.visit_union(*this);
+}
+
+mpz_class Union::count() const {
+  mpz_class c = 1;
+  for (const Ptr<TypeExpr> &m : members)
+    c += m->count();
+  return c;
+}
+
+bool Union::is_simple() const {
+  for (const Ptr<TypeExpr> &m : members) {
+    if (!m->is_simple())
+      return false;
+  }
+  return true;
+}
+
+void Union::validate() const {
+  // In contrast to CMurphi, we treat unions containing 0 or 1 members as legal.
+  // We also allow a single type to appear multiple times within the union.
+  // There is no known practical use for most of these edge cases, but it
+  // simplifies work for generators of Murphi models.
+}
+
+mpz_class Union::lower_bound() const {
+  if (!is_simple())
+    throw Error("union is not a simple type and thus its lower bound cannot be "
+                "determined",
+                loc);
+
+  mpz_class bound;
+  bool set = false;
+  for (const Ptr<TypeExpr> &m : members) {
+    const mpz_class b = m->lower_bound();
+    if (!set || b < bound)
+      bound = b;
+    set = true;
+  }
+
+  if (!set)
+    bound = 0;
+
+  return bound;
+}
+
+mpz_class Union::upper_bound() const {
+  if (!is_simple())
+    throw Error("union is not a simple type and thus its upper bound cannot be "
+                "determined",
+                loc);
+
+  mpz_class bound;
+  bool set = false;
+  for (const Ptr<TypeExpr> &m : members) {
+    const mpz_class b = m->upper_bound();
+    if (!set || b > bound)
+      bound = b;
+    set = true;
+  }
+
+  if (!set)
+    bound = 0;
+
+  return bound;
+}
+
+void Union::to_stream(std::ostream &out) const {
+  out << "union {";
+  const char *separator = "";
+  for (const Ptr<TypeExpr> &m : members) {
+    out << separator << *m;
+    separator = ", ";
+  }
+  out << "}";
+}
+
+bool Union::constant() const {
+  for (const Ptr<TypeExpr> &m : members) {
+    if (!m->is_simple())
+      return false;
+    if (!m->constant())
+      return false;
+  }
+  return true;
+}
+
 } // namespace rumur
diff --git a/librumur/src/indexer.cc b/librumur/src/indexer.cc
index fdbcbdca..e2cf265e 100644
--- a/librumur/src/indexer.cc
+++ b/librumur/src/indexer.cc
@@ -161,6 +161,12 @@ void Indexer::visit_ifclause(IfClause &n) {
 
 void Indexer::visit_implication(Implication &n) { visit_bexpr(n); }
 
+void Indexer::visit_ismember(IsMember &n) {
+  n.unique_id = next++;
+  dispatch(*n.peg);
+  dispatch(*n.hole);
+}
+
 void Indexer::visit_isundefined(IsUndefined &n) { visit_uexpr(n); }
 
 void Indexer::visit_leq(Leq &n) { visit_bexpr(n); }
@@ -326,6 +332,12 @@ void Indexer::visit_undefine(Undefine &n) {
   dispatch(*n.rhs);
 }
 
+void Indexer::visit_union(Union &n) {
+  n.unique_id = next++;
+  for (Ptr<TypeExpr> &m : n.members)
+    dispatch(*m);
+}
+
 void Indexer::visit_vardecl(VarDecl &n) {
   n.unique_id = next++;
   dispatch(*n.type);
diff --git a/librumur/src/lexer.l b/librumur/src/lexer.l
index 8b026bd1..e5bc910b 100644
--- a/librumur/src/lexer.l
+++ b/librumur/src/lexer.l
@@ -96,6 +96,7 @@ forall        { return rumur::parser::token::FORALL;        }
 function      { return rumur::parser::token::FUNCTION;      }
 if            { return rumur::parser::token::IF;            }
 invariant     { return rumur::parser::token::INVARIANT;     }
+ismember      { return rumur::parser::token::ISMEMBER;      }
 isundefined   { return rumur::parser::token::ISUNDEFINED;   }
 liveness      { return rumur::parser::token::LIVENESS;      }
 of            { return rumur::parser::token::OF;            }
@@ -113,7 +114,7 @@ then          { return rumur::parser::token::THEN;          }
 to            { return rumur::parser::token::TO;            }
 type          { return rumur::parser::token::TYPE;          }
 undefine      { return rumur::parser::token::UNDEFINE;      }
-union         { throw rumur::Error("union types are not supported", *loc); }
+union         { return rumur::parser::token::UNION;         }
 var           { return rumur::parser::token::VAR;           }
 while         { return rumur::parser::token::WHILE;         }
 
diff --git a/librumur/src/parser.yy b/librumur/src/parser.yy
index b7f33cc6..724fdc8b 100644
--- a/librumur/src/parser.yy
+++ b/librumur/src/parser.yy
@@ -154,6 +154,7 @@
 %token IF
 %token IMPLIES "->"
 %token INVARIANT
+%token ISMEMBER
 %token ISUNDEFINED
 %token LAND "∧"
 %token LEQ "<="
@@ -185,6 +186,7 @@
 %token TO
 %token TYPE
 %token UNDEFINE
+%token UNION
 %token VAR
 %token WHILE
 
@@ -241,6 +243,8 @@
 %type <std::vector<rumur::Ptr<rumur::Decl>>>                 typedecl
 %type <std::vector<rumur::Ptr<rumur::Decl>>>                 typedecls
 %type <rumur::Ptr<rumur::TypeExpr>>                          typeexpr
+%type <std::vector<rumur::Ptr<rumur::TypeExpr>>>             typeexprs
+%type <std::vector<rumur::Ptr<rumur::TypeExpr>>>             typeexprs_cont
 %type <std::vector<rumur::Ptr<rumur::VarDecl>>>              vardecl
 %type <std::vector<rumur::Ptr<rumur::VarDecl>>>              vardecls
 %type <std::shared_ptr<bool>>                                var_opt
@@ -433,6 +437,8 @@ expr: expr '?' expr ':' expr {
   $$->loc = @$;
 } | ID '(' exprlist ')' {
   $$ = rumur::Ptr<rumur::FunctionCall>::make($1, $3, @$);
+} | ISMEMBER '(' expr ',' typeexpr ')' {
+  $$ = rumur::Ptr<rumur::IsMember>::make($3, $5, @$);
 } | ISUNDEFINED '(' designator ')' {
   $$ = rumur::Ptr<rumur::IsUndefined>::make($3, @$);
 };
@@ -676,6 +682,22 @@ typeexpr: BOOLEAN {
   $$ = rumur::Ptr<rumur::Array>::make($3, $6, @$);
 } | SCALARSET '(' expr ')' {
   $$ = rumur::Ptr<rumur::Scalarset>::make($3, @$);
+} | UNION '{' typeexprs '}' {
+  $$ = rumur::Ptr<rumur::Union>::make($3, @$);
+};
+
+typeexprs: typeexprs_cont typeexpr comma_opt {
+  $$ = $1;
+  $$.push_back($2);
+} | %empty {
+  /* nothing required */
+};
+
+typeexprs_cont: typeexprs_cont typeexpr ',' {
+  $$ = $1;
+  $$.push_back($2);
+} | %empty {
+  /* nothing required */
 };
 
 vardecl: id_list_opt ':' typeexpr {
diff --git a/librumur/src/resolve-symbols.cc b/librumur/src/resolve-symbols.cc
index f6657084..7210bc36 100644
--- a/librumur/src/resolve-symbols.cc
+++ b/librumur/src/resolve-symbols.cc
@@ -234,6 +234,12 @@ class Resolver : public Traversal {
 
   void visit_implication(Implication &n) final { visit_bexpr(n); }
 
+  void visit_ismember(IsMember &n) final {
+    dispatch(*n.peg);
+    dispatch(*n.hole);
+    disambiguate(n.peg);
+  }
+
   void visit_isundefined(IsUndefined &n) final { visit_uexpr(n); }
 
   void visit_leq(Leq &n) final { visit_bexpr(n); }
diff --git a/librumur/src/traverse.cc b/librumur/src/traverse.cc
index ea071d70..e3dca41b 100644
--- a/librumur/src/traverse.cc
+++ b/librumur/src/traverse.cc
@@ -137,6 +137,11 @@ void Traversal::visit_ifclause(IfClause &n) {
 
 void Traversal::visit_implication(Implication &n) { visit_bexpr(n); }
 
+void Traversal::visit_ismember(IsMember &n) {
+  dispatch(*n.peg);
+  dispatch(*n.hole);
+}
+
 void Traversal::visit_isundefined(IsUndefined &n) { visit_uexpr(n); }
 
 void Traversal::visit_leq(Leq &n) { visit_bexpr(n); }
@@ -267,6 +272,11 @@ void Traversal::visit_uexpr(UnaryExpr &n) { dispatch(*n.rhs); }
 
 void Traversal::visit_undefine(Undefine &n) { dispatch(*n.rhs); }
 
+void Traversal::visit_union(Union &n) {
+  for (Ptr<TypeExpr> &m : n.members)
+    dispatch(*m);
+}
+
 void Traversal::visit_vardecl(VarDecl &n) {
   if (n.type != nullptr)
     dispatch(*n.type);
@@ -406,6 +416,11 @@ void ConstTraversal::visit_ifclause(const IfClause &n) {
 
 void ConstTraversal::visit_implication(const Implication &n) { visit_bexpr(n); }
 
+void ConstTraversal::visit_ismember(const IsMember &n) {
+  dispatch(*n.peg);
+  dispatch(*n.hole);
+}
+
 void ConstTraversal::visit_isundefined(const IsUndefined &n) { visit_uexpr(n); }
 
 void ConstTraversal::visit_leq(const Leq &n) { visit_bexpr(n); }
@@ -540,6 +555,11 @@ void ConstTraversal::visit_uexpr(const UnaryExpr &n) { dispatch(*n.rhs); }
 
 void ConstTraversal::visit_undefine(const Undefine &n) { dispatch(*n.rhs); }
 
+void ConstTraversal::visit_union(const Union &n) {
+  for (const Ptr<TypeExpr> &m : n.members)
+    dispatch(*m);
+}
+
 void ConstTraversal::visit_vardecl(const VarDecl &n) {
   if (n.type != nullptr)
     dispatch(*n.type);
@@ -728,6 +748,11 @@ void ConstExprTraversal::visit_typeexprid(const TypeExprID &) {}
 
 void ConstExprTraversal::visit_undefine(const Undefine &n) { dispatch(*n.rhs); }
 
+void ConstExprTraversal::visit_union(const Union &n) {
+  for (const Ptr<TypeExpr> &m : n.members)
+    dispatch(*m);
+}
+
 void ConstExprTraversal::visit_vardecl(const VarDecl &n) {
   if (n.type != nullptr)
     dispatch(*n.type);
@@ -830,6 +855,11 @@ void ConstStmtTraversal::visit_implication(const Implication &n) {
   visit_bexpr(n);
 }
 
+void ConstStmtTraversal::visit_ismember(const IsMember &n) {
+  dispatch(*n.peg);
+  dispatch(*n.hole);
+}
+
 void ConstStmtTraversal::visit_isundefined(const IsUndefined &n) {
   visit_uexpr(n);
 }
@@ -946,6 +976,11 @@ void ConstStmtTraversal::visit_typeexprid(const TypeExprID &) {}
 
 void ConstStmtTraversal::visit_uexpr(const UnaryExpr &n) { dispatch(*n.rhs); }
 
+void ConstStmtTraversal::visit_union(const Union &n) {
+  for (const Ptr<TypeExpr> &m : n.members)
+    dispatch(*m);
+}
+
 void ConstStmtTraversal::visit_vardecl(const VarDecl &n) {
   if (n.type != nullptr)
     dispatch(*n.type);
@@ -1064,6 +1099,11 @@ void ConstTypeTraversal::visit_implication(const Implication &n) {
   visit_bexpr(n);
 }
 
+void ConstTypeTraversal::visit_ismember(const IsMember &n) {
+  dispatch(*n.peg);
+  dispatch(*n.hole);
+}
+
 void ConstTypeTraversal::visit_isundefined(const IsUndefined &n) {
   visit_uexpr(n);
 }
diff --git a/librumur/src/validate.cc b/librumur/src/validate.cc
index 1b577814..31c7f785 100644
--- a/librumur/src/validate.cc
+++ b/librumur/src/validate.cc
@@ -207,6 +207,12 @@ class Validator : public ConstBaseTraversal {
     n.validate();
   }
 
+  void visit_ismember(const IsMember &n) final {
+    dispatch(*n.peg);
+    dispatch(*n.hole);
+    n.validate();
+  }
+
   void visit_isundefined(const IsUndefined &n) final {
     dispatch(*n.rhs);
     n.validate();
@@ -415,6 +421,12 @@ class Validator : public ConstBaseTraversal {
     n.validate();
   }
 
+  void visit_union(const Union &n) final {
+    for (const Ptr<TypeExpr> &m : n.members)
+      dispatch(*m);
+    n.validate();
+  }
+
   void visit_vardecl(const VarDecl &n) final {
     if (n.type != nullptr)
       dispatch(*n.type);
diff --git a/misc/murphi2xml.rng b/misc/murphi2xml.rng
index 5cda0fa3..ad6fe4f2 100644
--- a/misc/murphi2xml.rng
+++ b/misc/murphi2xml.rng
@@ -290,6 +290,7 @@
       <ref name="geq"/>
       <ref name="gt"/>
       <ref name="implication"/>
+      <ref name="ismember"/>
       <ref name="isundefined"/>
       <ref name="leq"/>
       <ref name="lsh"/>
@@ -497,6 +498,21 @@
     </element>
   </define>
 
+  <define name="ismember">
+    <element name="ismember">
+      <ref name="location"/>
+      <ref name="content"/>
+      <element name="arg0">
+        <ref name="expr"/>
+      </element>
+      <ref name="content"/>
+      <element name="arg1">
+        <ref name="typeexpr"/>
+      </element>
+      <ref name="content"/>
+    </element>
+  </define>
+
   <define name="isundefined">
     <element name="isundefined">
       <ref name="location"/>
@@ -1084,6 +1100,7 @@
       <ref name="record"/>
       <ref name="scalarset"/>
       <ref name="typeexprid"/>
+      <ref name="union"/>
     </choice>
   </define>
 
@@ -1116,6 +1133,17 @@
     </element>
   </define>
 
+  <define name="union">
+    <element name="union">
+      <ref name="location"/>
+      <ref name="content"/>
+      <zeroOrMore>
+        <ref name="typeexpr"/>
+        <ref name="content"/>
+      </zeroOrMore>
+    </element>
+  </define>
+
   <define name="unit">
     <element name="unit">
       <attribute name="filename">
diff --git a/murphi-format/src/format.c b/murphi-format/src/format.c
index ba7b5f16..75939879 100644
--- a/murphi-format/src/format.c
+++ b/murphi-format/src/format.c
@@ -289,6 +289,9 @@ static bool is_keyword(const char *text) {
   if (streq(text, "invariant"))
     return true;
 #if 0
+  // `ismember` is a keyword, but is used as if it were a function
+  if (streq(text, "ismember"))
+    return true;
   // `isundefined` is a keyword, but is used as if it were a function
   if (streq(text, "isundefined"))
     return true;
diff --git a/murphi2c/src/CLikeGenerator.cc b/murphi2c/src/CLikeGenerator.cc
index e13d244e..013d8639 100644
--- a/murphi2c/src/CLikeGenerator.cc
+++ b/murphi2c/src/CLikeGenerator.cc
@@ -377,6 +377,11 @@ void CLikeGenerator::visit_implication(const Implication &n) {
   *this << "(!" << *n.lhs << " || " << *n.rhs << ")";
 }
 
+void CLikeGenerator::visit_ismember(const IsMember &) {
+  assert(!"ismember was not rejected during check()");
+  __builtin_unreachable();
+}
+
 void CLikeGenerator::visit_isundefined(const IsUndefined &) {
   // check() prevents a model with isundefined expressions from making it
   // through to here
@@ -521,6 +526,8 @@ void CLikeGenerator::print(const std::string &suffix, const TypeExpr &t,
 
   const Ptr<TypeExpr> type = t.resolve();
 
+  assert(!isa<Union>(type) && "union type was not rejected during check()");
+
   // if this is boolean, handle it separately to other Enums to avoid
   // -Wswitch-bool warnings and cope with badly behaved users setting non-0/1
   // values
@@ -833,6 +840,11 @@ void CLikeGenerator::visit_undefine(const Undefine &n) {
   *this << "\n";
 }
 
+void CLikeGenerator::visit_union(const Union &) {
+  assert(!"union type was not rejected during check()");
+  __builtin_unreachable();
+}
+
 void CLikeGenerator::visit_while(const While &n) {
   *this << indentation() << "while " << *n.condition << " {\n";
   indent();
diff --git a/murphi2c/src/CLikeGenerator.h b/murphi2c/src/CLikeGenerator.h
index c9240011..fe0d6d09 100644
--- a/murphi2c/src/CLikeGenerator.h
+++ b/murphi2c/src/CLikeGenerator.h
@@ -64,6 +64,7 @@ class __attribute__((visibility("hidden"))) CLikeGenerator
   void visit_if(const rumur::If &n) final;
   void visit_ifclause(const rumur::IfClause &n) final;
   void visit_implication(const rumur::Implication &n) final;
+  void visit_ismember(const rumur::IsMember &) final;
   void visit_isundefined(const rumur::IsUndefined &) final;
   void visit_leq(const rumur::Leq &n) final;
   void visit_lsh(const rumur::Lsh &n) final;
@@ -94,6 +95,7 @@ class __attribute__((visibility("hidden"))) CLikeGenerator
   void visit_typedecl(const rumur::TypeDecl &n) final;
   void visit_typeexprid(const rumur::TypeExprID &n) final;
   void visit_undefine(const rumur::Undefine &n) final;
+  void visit_union(const rumur::Union &n) final;
   void visit_while(const rumur::While &n) final;
   void visit_xor(const rumur::Xor &n) final;
 
diff --git a/murphi2c/src/check.cc b/murphi2c/src/check.cc
index dda46b22..b57f824d 100644
--- a/murphi2c/src/check.cc
+++ b/murphi2c/src/check.cc
@@ -13,12 +13,26 @@ class Check : public ConstTraversal {
 public:
   bool ok = true;
 
+  void visit_ismember(const IsMember &) final {
+    if (ok) {
+      std::cerr << "ismember expressions are not supported\n";
+      ok = false;
+    }
+  }
+
   void visit_isundefined(const IsUndefined &) final {
     if (ok) {
       std::cerr << "isundefined expressions are not supported\n";
       ok = false;
     }
   }
+
+  void visit_union(const Union &) final {
+    if (ok) {
+      std::cerr << "union types are not supported\n";
+      ok = false;
+    }
+  }
 };
 
 } // namespace
diff --git a/murphi2murphi/src/DecomposeComplexComparisons.cc b/murphi2murphi/src/DecomposeComplexComparisons.cc
index ab9c5b71..df80cf53 100644
--- a/murphi2murphi/src/DecomposeComplexComparisons.cc
+++ b/murphi2murphi/src/DecomposeComplexComparisons.cc
@@ -1,4 +1,5 @@
 #include "DecomposeComplexComparisons.h"
+#include "../../common/isa.h"
 #include "Stage.h"
 #include <cassert>
 #include <climits>
@@ -66,6 +67,13 @@ static std::string explode(std::unordered_set<std::string> &ids,
 
   const Ptr<TypeExpr> t = type.resolve();
 
+  // if this is a union, assume there is no reasonable way to decompose its
+  // comparison
+  if (isa<Union>(t)) {
+    buf << prefix_a << stem << (is_eq ? " = " : " != ") << prefix_b << stem;
+    return buf.str();
+  }
+
   // if this is a record, join together a comparison of each of its fields
   if (auto r = dynamic_cast<const Record *>(t.get())) {
     std::string sep;
@@ -99,12 +107,15 @@ void DecomposeComplexComparisons::rewrite(const EquatableBinaryExpr &n,
                                           bool is_eq) {
 
   // if this is a comparison of simple types, we can let it pass through
-  const Ptr<TypeExpr> t = n.lhs->type();
-  if (t->is_simple()) {
-
-    assert(n.rhs->type()->is_simple() &&
-           "comparison of simple type to complex type");
+  const Ptr<TypeExpr> lhs_type = n.lhs->type();
+  const Ptr<TypeExpr> rhs_type = n.rhs->type();
+  if (lhs_type->is_simple() && rhs_type->is_simple()) {
+    next.dispatch(n);
+    return;
+  }
 
+  // is either side is of union type, we cannot decompose this
+  if (isa<Union>(lhs_type) || isa<Union>(rhs_type)) {
     next.dispatch(n);
     return;
   }
@@ -133,5 +144,6 @@ void DecomposeComplexComparisons::rewrite(const EquatableBinaryExpr &n,
   ids.insert(rhs_ids.begin(), rhs_ids.end());
 
   // write a decomposed version of the comparison
-  *top << explode(ids, n.lhs->to_string(), n.rhs->to_string(), "", *t, is_eq);
+  *top << explode(ids, n.lhs->to_string(), n.rhs->to_string(), "", *lhs_type,
+                  is_eq);
 }
diff --git a/murphi2murphi/src/Printer.cc b/murphi2murphi/src/Printer.cc
index 20f9318c..1167df63 100644
--- a/murphi2murphi/src/Printer.cc
+++ b/murphi2murphi/src/Printer.cc
@@ -236,6 +236,15 @@ void Printer::visit_ifclause(const IfClause &n) {
 
 void Printer::visit_implication(const Implication &n) { visit_bexpr(n); }
 
+void Printer::visit_ismember(const IsMember &n) {
+  top->sync_to(n);
+  top->sync_to(*n.peg);
+  top->dispatch(*n.peg);
+  top->sync_to(*n.hole);
+  top->dispatch(*n.hole);
+  top->sync_to(n.loc.end);
+}
+
 void Printer::visit_isundefined(const IsUndefined &n) { visit_uexpr(n); }
 
 void Printer::visit_leq(const Leq &n) { visit_bexpr(n); }
@@ -513,6 +522,15 @@ void Printer::visit_undefine(const Undefine &n) {
   top->sync_to(n.loc.end);
 }
 
+void Printer::visit_union(const Union &n) {
+  top->sync_to(n);
+  for (const Ptr<TypeExpr> &m : n.members) {
+    top->sync_to(*m);
+    top->dispatch(*m);
+  }
+  top->sync_to(n.loc.end);
+}
+
 void Printer::visit_vardecl(const VarDecl &n) {
   top->sync_to(n);
   top->sync_to(*n.type);
diff --git a/murphi2murphi/src/Printer.h b/murphi2murphi/src/Printer.h
index 4de85f70..c1bc53d6 100644
--- a/murphi2murphi/src/Printer.h
+++ b/murphi2murphi/src/Printer.h
@@ -47,6 +47,7 @@ class Printer : public Stage {
   void visit_if(const rumur::If &n) final;
   void visit_ifclause(const rumur::IfClause &n) final;
   void visit_implication(const rumur::Implication &n) final;
+  void visit_ismember(const rumur::IsMember &n) final;
   void visit_isundefined(const rumur::IsUndefined &n) final;
   void visit_leq(const rumur::Leq &n) final;
   void visit_lsh(const rumur::Lsh &n) final;
@@ -80,6 +81,7 @@ class Printer : public Stage {
   void visit_typedecl(const rumur::TypeDecl &n) final;
   void visit_typeexprid(const rumur::TypeExprID &n) final;
   void visit_undefine(const rumur::Undefine &n) final;
+  void visit_union(const rumur::Union &n) final;
   void visit_vardecl(const rumur::VarDecl &n) final;
   void visit_while(const rumur::While &n) final;
   void visit_xor(const rumur::Xor &n) final;
diff --git a/murphi2murphi/src/Stage.cc b/murphi2murphi/src/Stage.cc
index 83df4e79..51839870 100644
--- a/murphi2murphi/src/Stage.cc
+++ b/murphi2murphi/src/Stage.cc
@@ -120,6 +120,9 @@ void IntermediateStage::visit_ifclause(const IfClause &n) {
 void IntermediateStage::visit_implication(const Implication &n) {
   next.visit_implication(n);
 }
+void IntermediateStage::visit_ismember(const IsMember &n) {
+  next.visit_ismember(n);
+}
 void IntermediateStage::visit_isundefined(const IsUndefined &n) {
   next.visit_isundefined(n);
 }
@@ -185,6 +188,7 @@ void IntermediateStage::visit_typeexprid(const TypeExprID &n) {
 void IntermediateStage::visit_undefine(const Undefine &n) {
   next.visit_undefine(n);
 }
+void IntermediateStage::visit_union(const Union &n) { next.visit_union(n); }
 void IntermediateStage::visit_vardecl(const VarDecl &n) {
   next.visit_vardecl(n);
 }
diff --git a/murphi2murphi/src/Stage.h b/murphi2murphi/src/Stage.h
index f623fe23..635d736f 100644
--- a/murphi2murphi/src/Stage.h
+++ b/murphi2murphi/src/Stage.h
@@ -89,6 +89,7 @@ class IntermediateStage : public Stage {
   void visit_if(const rumur::If &n) override;
   void visit_ifclause(const rumur::IfClause &n) override;
   void visit_implication(const rumur::Implication &n) override;
+  void visit_ismember(const rumur::IsMember &n) override;
   void visit_isundefined(const rumur::IsUndefined &n) override;
   void visit_leq(const rumur::Leq &n) override;
   void visit_lsh(const rumur::Lsh &n) override;
@@ -122,6 +123,7 @@ class IntermediateStage : public Stage {
   void visit_typedecl(const rumur::TypeDecl &n) override;
   void visit_typeexprid(const rumur::TypeExprID &n) override;
   void visit_undefine(const rumur::Undefine &n) override;
+  void visit_union(const rumur::Union &n) override;
   void visit_vardecl(const rumur::VarDecl &n) override;
   void visit_while(const rumur::While &n) override;
   void visit_xor(const rumur::Xor &n) override;
diff --git a/murphi2smv/doc/murphi2smv.1 b/murphi2smv/doc/murphi2smv.1
index 21b39229..0238859a 100644
--- a/murphi2smv/doc/murphi2smv.1
+++ b/murphi2smv/doc/murphi2smv.1
@@ -97,6 +97,8 @@ simple \fBrule\fRs
 .IP \[bu]
 \fBundefine\fR statements
 .IP \[bu]
+\fBunion\fR types
+.IP \[bu]
 \fBwhile\fR statements
 .RE
 .PP
diff --git a/murphi2smv/src/codegen.cc b/murphi2smv/src/codegen.cc
index 913c1417..0abd922a 100644
--- a/murphi2smv/src/codegen.cc
+++ b/murphi2smv/src/codegen.cc
@@ -244,6 +244,12 @@ class Printer : public ConstBaseTraversal {
     *this << '(' << *n.lhs << " -> " << *n.rhs << ')';
   }
 
+  void visit_ismember(const IsMember &n) final {
+    *this << "/-- FIXME: Murphi ismember expressions have no equivalent in SMV "
+             "--/ ismember("
+          << *n.peg << ", " << *n.hole << ")";
+  }
+
   void visit_isundefined(const IsUndefined &n) final {
     *this << tab()
           << "/-- FIXME: Murphi isundefined statements have no equivalent in "
@@ -542,6 +548,20 @@ class Printer : public ConstBaseTraversal {
         << *n.rhs << "` --/\n";
   }
 
+  void visit_union(const Union &n) final {
+    *this << tab()
+          << "/-- FIXME: Murphi union types have no equivalent in SMV --/\n";
+
+    indent();
+    for (const Ptr<TypeExpr> &m : n.members) {
+      emit_leading_comments(*m);
+      *this << *m;
+    }
+    dedent();
+
+    *this << tab() << "/-- FIXME: end of union type --/\n";
+  }
+
   void visit_vardecl(const VarDecl &n) final {
     *this << tab() << "VAR " << n.name << " : " << *n.get_type() << ";\n";
   }
diff --git a/murphi2uclid/doc/murphi2uclid.1 b/murphi2uclid/doc/murphi2uclid.1
index 9dd1a678..1a353fc3 100644
--- a/murphi2uclid/doc/murphi2uclid.1
+++ b/murphi2uclid/doc/murphi2uclid.1
@@ -67,6 +67,8 @@ Aliases, in the form of declarations statements or rules
 .IP \[bu]
 The \fBisundefined\fR operator
 .IP \[bu]
+\fBunion\fR types
+.IP \[bu]
 The modulo operator, \fB%\fR
 .IP \[bu]
 The left and shift shift operators, \fB<<\fR and \fB>>\fR
diff --git a/murphi2uclid/src/check.cc b/murphi2uclid/src/check.cc
index 1c30a7c0..4a65a048 100644
--- a/murphi2uclid/src/check.cc
+++ b/murphi2uclid/src/check.cc
@@ -115,6 +115,10 @@ class Checker : public ConstTraversal {
       n.body.back()->visit(*this);
   }
 
+  void visit_ismember(const IsMember &n) final {
+    throw Error("Uclid5 has no equivalent of the ismember function", n.loc);
+  }
+
   void visit_lsh(const Lsh &n) final {
     // TODO: technically we could implement this as a Uclid5 function. However,
     // it is a little awkward because Uclid5 does not support generic functions
@@ -268,6 +272,10 @@ class Checker : public ConstTraversal {
       n.body.back()->visit(*this);
   }
 
+  void visit_union(const Union &n) final {
+    throw Error("Uclid5 has no equivalent of union types", n.loc);
+  }
+
   void visit_while(const While &n) final {
     n.condition->visit(*this);
 
diff --git a/murphi2uclid/src/codegen.cc b/murphi2uclid/src/codegen.cc
index 9c3e6081..74a8918a 100644
--- a/murphi2uclid/src/codegen.cc
+++ b/murphi2uclid/src/codegen.cc
@@ -433,6 +433,11 @@ class Printer : public ConstBaseTraversal {
     *this << "(" << *n.lhs << " ==> " << *n.rhs << ")";
   }
 
+  void visit_ismember(const IsMember &) final {
+    assert(!"ismember not rejected during check()");
+    __builtin_unreachable();
+  }
+
   void visit_isundefined(const IsUndefined &) final {
     assert(!"isundefined not rejected during check()");
     __builtin_unreachable();
@@ -953,6 +958,11 @@ class Printer : public ConstBaseTraversal {
     *this << tab() << "havoc " << *n.rhs << ";\n";
   }
 
+  void visit_union(const Union &) final {
+    assert(!"union type not rejected during check()");
+    __builtin_unreachable();
+  }
+
   void visit_vardecl(const VarDecl &n) final {
     *this << tab() << "var " << n.name << " : " << *n.get_type() << ";\n";
 
diff --git a/murphi2xml/src/XMLPrinter.cc b/murphi2xml/src/XMLPrinter.cc
index d1137b93..0dad71c5 100644
--- a/murphi2xml/src/XMLPrinter.cc
+++ b/murphi2xml/src/XMLPrinter.cc
@@ -419,6 +419,23 @@ void XMLPrinter::visit_implication(const Implication &n) {
   visit_bexpr("implication", n);
 }
 
+void XMLPrinter::visit_ismember(const IsMember &n) {
+  sync_to(n);
+  o << "<ismember ";
+  add_location(n);
+  o << ">";
+  sync_to(*n.peg);
+  o << "<arg0>";
+  dispatch(*n.peg);
+  o << "</arg0>";
+  sync_to(*n.hole);
+  o << "<arg1>";
+  dispatch(*n.hole);
+  o << "</arg1>";
+  sync_to(n.loc.end);
+  o << "</ismember>";
+}
+
 void XMLPrinter::visit_isundefined(const IsUndefined &n) {
   visit_uexpr("isundefined", n);
 }
@@ -849,6 +866,19 @@ void XMLPrinter::visit_undefine(const Undefine &n) {
   o << "</undefine>";
 }
 
+void XMLPrinter::visit_union(const Union &n) {
+  sync_to(n);
+  o << "<union ";
+  add_location(n);
+  o << ">";
+  for (const Ptr<TypeExpr> &m : n.members) {
+    sync_to(*m);
+    dispatch(*m);
+  }
+  sync_to(n.loc.end);
+  o << "</union>";
+}
+
 void XMLPrinter::visit_vardecl(const VarDecl &n) {
   sync_to(n);
   o << "<vardecl name=\"" << n.name << "\" readonly=\"" << n.readonly << "\" ";
diff --git a/murphi2xml/src/XMLPrinter.h b/murphi2xml/src/XMLPrinter.h
index 06887830..2f333577 100644
--- a/murphi2xml/src/XMLPrinter.h
+++ b/murphi2xml/src/XMLPrinter.h
@@ -46,6 +46,7 @@ class XMLPrinter : public rumur::ConstBaseTraversal {
   void visit_if(const rumur::If &n) final;
   void visit_ifclause(const rumur::IfClause &n) final;
   void visit_implication(const rumur::Implication &n) final;
+  void visit_ismember(const rumur::IsMember &n) final;
   void visit_isundefined(const rumur::IsUndefined &n) final;
   void visit_leq(const rumur::Leq &n) final;
   void visit_lsh(const rumur::Lsh &n) final;
@@ -79,6 +80,7 @@ class XMLPrinter : public rumur::ConstBaseTraversal {
   void visit_typedecl(const rumur::TypeDecl &n) final;
   void visit_typeexprid(const rumur::TypeExprID &n) final;
   void visit_undefine(const rumur::Undefine &n) final;
+  void visit_union(const rumur::Union &n) final;
   void visit_vardecl(const rumur::VarDecl &n) final;
   void visit_while(const rumur::While &n) final;
   void visit_xor(const rumur::Xor &n) final;
diff --git a/rumur/CMakeLists.txt b/rumur/CMakeLists.txt
index 04dda2f3..4b859c5b 100644
--- a/rumur/CMakeLists.txt
+++ b/rumur/CMakeLists.txt
@@ -25,6 +25,7 @@ add_executable(rumur
   ../common/escape.cc
   ../common/help.c
   src/assume-statements-count.cc
+  src/check.cc
   src/generate-allocations.cc
   src/generate-cover-array.cc
   src/generate-decl.cc
diff --git a/rumur/src/check.cc b/rumur/src/check.cc
new file mode 100644
index 00000000..25558b47
--- /dev/null
+++ b/rumur/src/check.cc
@@ -0,0 +1,24 @@
+#include "check.h"
+#include <rumur/rumur.h>
+
+using namespace rumur;
+
+namespace {
+
+class Check : public ConstTraversal {
+
+public:
+  void visit_ismember(const IsMember &n) final {
+    throw Error("ismember expressions are not supported", n.loc);
+  }
+
+  void visit_union(const Union &n) final {
+    throw Error("union types are not supported", n.loc);
+  }
+};
+} // namespace
+
+void check(const rumur::Node &n) {
+  Check c;
+  c.dispatch(n);
+}
diff --git a/rumur/src/check.h b/rumur/src/check.h
new file mode 100644
index 00000000..486337a1
--- /dev/null
+++ b/rumur/src/check.h
@@ -0,0 +1,6 @@
+#pragma once
+
+#include <rumur/rumur.h>
+
+/// throw a `rumur::Error` if the given node contains anything unsupported
+void check(const rumur::Node &n);
diff --git a/rumur/src/generate-expr.cc b/rumur/src/generate-expr.cc
index e0547498..e78fa04c 100644
--- a/rumur/src/generate-expr.cc
+++ b/rumur/src/generate-expr.cc
@@ -469,6 +469,11 @@ class Generator : public ConstExprTraversal {
     *this << "(!" << *n.lhs << " || " << *n.rhs << ")";
   }
 
+  void visit_ismember(const IsMember &) final {
+    assert(!"ismember expression not rejected before code generation");
+    __builtin_unreachable();
+  }
+
   void visit_isundefined(const IsUndefined &n) final {
     *this << "handle_isundefined(s, ";
     generate_lvalue(*out, *n.rhs);
diff --git a/rumur/src/generate-print.cc b/rumur/src/generate-print.cc
index af3d31f9..0c25e4e2 100644
--- a/rumur/src/generate-print.cc
+++ b/rumur/src/generate-print.cc
@@ -1,4 +1,5 @@
 #include "../../common/escape.h"
+#include "../../common/isa.h"
 #include "generate.h"
 #include "options.h"
 #include <cassert>
@@ -316,6 +317,8 @@ class Generator : public ConstTypeTraversal {
       return;
     }
 
+    assert(!isa<Union>(t) && "union type not rejected before code generation");
+
     assert(!"non-range, non-enum used as array index");
   }
 
@@ -516,6 +519,10 @@ class Generator : public ConstTypeTraversal {
 
     dispatch(*n.referent->value);
   }
+
+  void visit_union(const Union &n) final {
+    throw Error("union types are not supported", n.loc);
+  }
 };
 
 } // namespace
diff --git a/rumur/src/generate-stmt.cc b/rumur/src/generate-stmt.cc
index 12bb48ef..ed3bdd28 100644
--- a/rumur/src/generate-stmt.cc
+++ b/rumur/src/generate-stmt.cc
@@ -72,6 +72,13 @@ static void clear(std::ostream &out, const TypeExpr &t,
     return;
   }
 
+  if (auto u = dynamic_cast<const Union *>(type.get())) {
+    // Generate a clear for each interpretation of this type. This is not
+    // efficient, but at least simple.
+    for (const Ptr<TypeExpr> &m : u->members)
+      clear(out, *m, offset, depth);
+  }
+
   assert(!"unreachable");
 }
 
diff --git a/rumur/src/main.cc b/rumur/src/main.cc
index ba1be689..7725c37d 100644
--- a/rumur/src/main.cc
+++ b/rumur/src/main.cc
@@ -1,6 +1,7 @@
 #include "../../common/environ.h"
 #include "../../common/help.h"
 #include "ValueType.h"
+#include "check.h"
 #include "generate.h"
 #include "has-start-state.h"
 #include "log.h"
@@ -671,6 +672,18 @@ int main(int argc, char **argv) {
   if (!has_start_state(*m))
     *warn << "warning: model has no start state\n";
 
+  // check whether the model uses unsupported things
+  try {
+    *debug << "checking for use of unsupported features...\n";
+    check(*m);
+  } catch (Error &e) {
+    std::cerr << white() << bold() << input_filename << ':' << e.loc << ':'
+              << reset() << ' ' << red() << bold() << "error:" << reset() << ' '
+              << white() << bold() << e.what() << reset() << '\n';
+    print_location(input_filename, e.loc);
+    return EXIT_FAILURE;
+  }
+
   // run SMT simplification if the user enabled it
   if (options.smt.simplification == SmtSimplification::ON) {
     *debug << "SMT simplification...\n";
diff --git a/rumur/src/smt/define-enum-members.cc b/rumur/src/smt/define-enum-members.cc
index 7ab8d4f3..4f1948d3 100644
--- a/rumur/src/smt/define-enum-members.cc
+++ b/rumur/src/smt/define-enum-members.cc
@@ -68,6 +68,12 @@ class Definer : public ConstTypeTraversal {
   void visit_scalarset(const Scalarset &) final {
     // as a primitive, scalarsets can't contain any enum members
   }
+
+  void visit_union(const Union &n) final {
+    // define any enum members that occur within union members
+    for (const Ptr<TypeExpr> &m : n.members)
+      dispatch(*m);
+  }
 };
 } // namespace
 
diff --git a/rumur/src/smt/define-records.cc b/rumur/src/smt/define-records.cc
index 3dc68c37..49db5700 100644
--- a/rumur/src/smt/define-records.cc
+++ b/rumur/src/smt/define-records.cc
@@ -63,6 +63,12 @@ class Definer : public ConstTypeTraversal {
   void visit_scalarset(const Scalarset &) final {
     // nothing to do
   }
+
+  void visit_union(const Union &n) final {
+    // define any records that are defined within this union
+    for (const Ptr<TypeExpr> &m : n.members)
+      dispatch(*m);
+  }
 };
 } // namespace
 
diff --git a/rumur/src/smt/simplify.cc b/rumur/src/smt/simplify.cc
index 7a9c89e8..647ce14b 100644
--- a/rumur/src/smt/simplify.cc
+++ b/rumur/src/smt/simplify.cc
@@ -194,6 +194,13 @@ class Simplifier : public BaseTraversal {
   }
 
   void visit_implication(Implication &n) final { visit_bexpr(n); }
+
+  void visit_ismember(IsMember &n) final {
+    dispatch(*n.peg);
+    simplify(n.peg);
+    dispatch(*n.hole);
+  }
+
   void visit_isundefined(IsUndefined &n) final { visit_uexpr(n); }
   void visit_leq(Leq &n) final { visit_bexpr(n); }
   void visit_lsh(Lsh &n) final { visit_bexpr(n); }
@@ -387,6 +394,11 @@ class Simplifier : public BaseTraversal {
 
   void visit_undefine(Undefine &n) final { dispatch(*n.rhs); }
 
+  void visit_union(Union &n) final {
+    for (Ptr<TypeExpr> &m : n.members)
+      dispatch(*m);
+  }
+
   void visit_vardecl(VarDecl &n) final { dispatch(*n.type); }
 
   void visit_while(While &n) final {
@@ -585,6 +597,12 @@ class Simplifier : public BaseTraversal {
         }
       }
 
+      void visit_union(const Union &) final {
+        // TODO: the constraints on a union should probably be the intersection
+        // of constraints on the union’s members
+        throw Unsupported();
+      }
+
       void visit_typeexprid(const TypeExprID &) final {
         assert(!"unreachable");
       }
diff --git a/rumur/src/smt/translate.cc b/rumur/src/smt/translate.cc
index ae100961..42412d90 100644
--- a/rumur/src/smt/translate.cc
+++ b/rumur/src/smt/translate.cc
@@ -105,6 +105,7 @@ class Translator : public ConstExprTraversal {
     *this << "(=> " << *n.lhs << " " << *n.rhs << ")";
   }
 
+  void visit_ismember(const IsMember &n) final { throw Unsupported(n); }
   void visit_isundefined(const IsUndefined &n) final { throw Unsupported(n); }
 
   void visit_leq(const Leq &n) final {
@@ -170,6 +171,7 @@ class Translator : public ConstExprTraversal {
 
     // determine the parts of the expression we will construct that depend on
     // forall
+    // clang-format off
     const std::string binder  = forall ? "forall" : "exists";
     const std::string op      = forall ? "or"     : "and";
     const std::string lb_rel  = forall ? lt()     : geq();
@@ -177,6 +179,7 @@ class Translator : public ConstExprTraversal {
     const std::string ub_rel2 = forall ? geq()    : lt();
     const std::string step_o  = forall ? "(not "  : "";
     const std::string step_c  = forall ? ")"      : "";
+    // clang-format on
 
     // “∀q.”/“∃q.”
     *this << "(" << binder << " ((" << qname << " " << qtype << ")) (" << op;
diff --git a/rumur/src/smt/typeexpr-to-smt.cc b/rumur/src/smt/typeexpr-to-smt.cc
index 3d4d4af9..13105337 100644
--- a/rumur/src/smt/typeexpr-to-smt.cc
+++ b/rumur/src/smt/typeexpr-to-smt.cc
@@ -74,6 +74,10 @@ class Translator : public ConstTypeTraversal {
     assert(n.referent != nullptr && "unresolved TypeExprID in AST");
     *this << *n.referent->value;
   }
+
+  void visit_union(const Union &) final {
+    throw Unsupported("union types are not supported in SMT translation");
+  }
 };
 } // namespace
 
diff --git a/rumur/src/symmetry-reduction.cc b/rumur/src/symmetry-reduction.cc
index 341995fd..b48a0613 100644
--- a/rumur/src/symmetry-reduction.cc
+++ b/rumur/src/symmetry-reduction.cc
@@ -113,6 +113,8 @@ static void generate_apply_swap(std::ostream &out, const std::string &offset_a,
     return;
   }
 
+  assert(!isa<Union>(t) && "union type not rejected before symmetry reduction");
+
   assert(!"missed case in generate_apply_swap");
 }
 
@@ -198,6 +200,9 @@ static void generate_swap_chunk(std::ostream &out, const TypeExpr &t,
     return;
   }
 
+  assert(!isa<Union>(type) &&
+         "union type not rejected before symmetry reduction");
+
   assert(!"missed case in generate_swap_chunk");
 }
 
@@ -467,6 +472,8 @@ static void generate_apply_compare(std::ostream &out, const TypeExpr &type,
     return;
   }
 
+  assert(!isa<Union>(t) && "union type not rejected before symmetry reduction");
+
   assert(!"missed case in generate_apply_compare");
 }
 
@@ -576,6 +583,9 @@ static void generate_compare_chunk(std::ostream &out, const TypeExpr &t,
     return;
   }
 
+  assert(!isa<Union>(type) &&
+         "union type not rejected before symmetry reduction");
+
   assert(!"missed case in generate_compare_chunk");
 }