diff --git a/src/cbmc/counterexample_beautification.cpp b/src/cbmc/counterexample_beautification.cpp
index c0e5d1ba230..a65069618df 100644
--- a/src/cbmc/counterexample_beautification.cpp
+++ b/src/cbmc/counterexample_beautification.cpp
@@ -40,7 +40,7 @@ void counterexample_beautificationt::get_minimization_list(
       it!=equation.SSA_steps.end(); it++)
   {
     if(it->is_assignment() &&
-       it->assignment_type==symex_targett::STATE)
+       it->assignment_type==symex_targett::assignment_typet::STATE)
     {
       if(!prop_conv.l_get(it->guard_literal).is_false())
       {
@@ -136,7 +136,7 @@ void counterexample_beautificationt::operator()(
         it!=equation.SSA_steps.end(); it++)
     {
       if(it->is_assignment() &&
-         it->assignment_type!=symex_targett::HIDDEN)
+         it->assignment_type!=symex_targett::assignment_typet::HIDDEN)
       {
         if(!it->guard_literal.is_constant())
           guard_count[it->guard_literal]++;
diff --git a/src/cbmc/fault_localization.cpp b/src/cbmc/fault_localization.cpp
index 9fa6651c1c8..7e1312df3d3 100644
--- a/src/cbmc/fault_localization.cpp
+++ b/src/cbmc/fault_localization.cpp
@@ -64,7 +64,7 @@ void fault_localizationt::collect_guards(lpointst &lpoints)
       it!=bmc.equation.SSA_steps.end(); it++)
   {
     if(it->is_assignment() &&
-       it->assignment_type==symex_targett::STATE &&
+       it->assignment_type==symex_targett::assignment_typet::STATE &&
        !it->ignore)
     {
       if(!it->guard_literal.is_constant())
diff --git a/src/goto-symex/build_goto_trace.cpp b/src/goto-symex/build_goto_trace.cpp
index 081fcbe55d3..f5b5375282d 100644
--- a/src/goto-symex/build_goto_trace.cpp
+++ b/src/goto-symex/build_goto_trace.cpp
@@ -300,9 +300,13 @@ void build_goto_trace(
 
     // drop PHI and GUARD assignments altogether
     if(it->is_assignment() &&
-       (SSA_step.assignment_type==symex_target_equationt::PHI ||
-        SSA_step.assignment_type==symex_target_equationt::GUARD))
+       (SSA_step.assignment_type==
+          symex_target_equationt::assignment_typet::PHI ||
+        SSA_step.assignment_type==
+          symex_target_equationt::assignment_typet::GUARD))
+    {
       continue;
+    }
 
     goto_tracet::stepst &steps=time_map[current_time];
     steps.push_back(goto_trace_stept());
@@ -330,8 +334,10 @@ void build_goto_trace(
 
     goto_trace_step.assignment_type=
       (it->is_assignment()&&
-       (SSA_step.assignment_type==symex_targett::VISIBLE_ACTUAL_PARAMETER ||
-        SSA_step.assignment_type==symex_targett::HIDDEN_ACTUAL_PARAMETER))?
+       (SSA_step.assignment_type==
+          symex_targett::assignment_typet::VISIBLE_ACTUAL_PARAMETER ||
+        SSA_step.assignment_type==
+          symex_targett::assignment_typet::HIDDEN_ACTUAL_PARAMETER))?
       goto_trace_stept::ACTUAL_PARAMETER:
       goto_trace_stept::STATE;
 
diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp
index e1a8938d823..7b9b206902b 100644
--- a/src/goto-symex/goto_symex_state.cpp
+++ b/src/goto-symex/goto_symex_state.cpp
@@ -759,7 +759,7 @@ bool goto_symex_statet::l2_thread_read_encoding(
       ssa_l1.get_original_expr(),
       tmp,
       source,
-      symex_targett::PHI);
+      symex_targett::assignment_typet::PHI);
 
     set_ssa_indices(ssa_l1, ns, L2);
     expr=ssa_l1;
diff --git a/src/goto-symex/slice_by_trace.cpp b/src/goto-symex/slice_by_trace.cpp
index 096edf8ae38..10936d28278 100644
--- a/src/goto-symex/slice_by_trace.cpp
+++ b/src/goto-symex/slice_by_trace.cpp
@@ -630,7 +630,7 @@ void symex_slice_by_tracet::assign_merges(
     SSA_step.guard=t_guard.as_expr();
     SSA_step.ssa_lhs=merge_sym;
     SSA_step.ssa_rhs.swap(merge_copy);
-    SSA_step.assignment_type=symex_targett::HIDDEN;
+    SSA_step.assignment_type=symex_targett::assignment_typet::HIDDEN;
 
     SSA_step.cond_expr=equal_exprt(SSA_step.ssa_lhs, SSA_step.ssa_rhs);
     SSA_step.type=goto_trace_stept::ASSIGNMENT;
diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp
index 795e1240f32..61b6ad28488 100644
--- a/src/goto-symex/symex_assign.cpp
+++ b/src/goto-symex/symex_assign.cpp
@@ -93,21 +93,21 @@ void goto_symext::symex_assign(
   }
   else
   {
-    assignment_typet assignment_type=symex_targett::STATE;
+    assignment_typet assignment_type=symex_targett::assignment_typet::STATE;
 
     // Let's hide return value assignments.
     if(lhs.id()==ID_symbol &&
        id2string(to_symbol_expr(lhs).get_identifier()).find(
                   "#return_value!")!=std::string::npos)
-      assignment_type=symex_targett::HIDDEN;
+      assignment_type=symex_targett::assignment_typet::HIDDEN;
 
     // We hide if we are in a hidden function.
     if(state.top().hidden_function)
-      assignment_type=symex_targett::HIDDEN;
+      assignment_type=symex_targett::assignment_typet::HIDDEN;
 
     // We hide if we are executing a hidden instruction.
     if(state.source.pc->source_location.get_hide())
-      assignment_type=symex_targett::HIDDEN;
+      assignment_type=symex_targett::assignment_typet::HIDDEN;
 
     guardt guard; // NOT the state guard!
     symex_assign_rec(state, lhs, nil_exprt(), rhs, guard, assignment_type);
@@ -303,7 +303,7 @@ void goto_symext::symex_assign_symbol(
   // do the assignment
   const symbolt &symbol=ns.lookup(ssa_lhs.get_original_expr());
   if(symbol.is_auxiliary)
-    assignment_type=symex_targett::HIDDEN;
+    assignment_type=symex_targett::assignment_typet::HIDDEN;
 
   target.assignment(
     tmp_guard.as_expr(),
diff --git a/src/goto-symex/symex_decl.cpp b/src/goto-symex/symex_decl.cpp
index b0b490b42b9..90d1f5f58f2 100644
--- a/src/goto-symex/symex_decl.cpp
+++ b/src/goto-symex/symex_decl.cpp
@@ -120,7 +120,9 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
     state.guard.as_expr(),
     ssa,
     state.source,
-    hidden?symex_targett::HIDDEN:symex_targett::STATE);
+    hidden ?
+      symex_targett::assignment_typet::HIDDEN :
+      symex_targett::assignment_typet::STATE);
 
   assert(state.dirty);
   if((*state.dirty)(ssa.get_object_name()) &&
diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp
index 8b36cfc26af..0f6328bdc44 100644
--- a/src/goto-symex/symex_goto.cpp
+++ b/src/goto-symex/symex_goto.cpp
@@ -184,7 +184,7 @@ void goto_symext::symex_goto(statet &state)
         new_lhs, new_lhs, guard_symbol_expr,
         new_rhs,
         original_source,
-        symex_targett::GUARD);
+        symex_targett::assignment_typet::GUARD);
 
       guard_expr=guard_symbol_expr;
       guard_expr.make_not();
@@ -437,7 +437,7 @@ void goto_symext::phi_function(
       new_lhs, new_lhs, new_lhs.get_original_expr(),
       rhs,
       dest_state.source,
-      symex_targett::PHI);
+      symex_targett::assignment_typet::PHI);
   }
 }
 
diff --git a/src/goto-symex/symex_start_thread.cpp b/src/goto-symex/symex_start_thread.cpp
index eb4687a1fb9..67cb147964c 100644
--- a/src/goto-symex/symex_start_thread.cpp
+++ b/src/goto-symex/symex_start_thread.cpp
@@ -94,7 +94,12 @@ void goto_symext::symex_start_thread(statet &state)
     const bool record_events=state.record_events;
     state.record_events=false;
     symex_assign_symbol(
-      state, lhs, nil_exprt(), rhs, guard, symex_targett::HIDDEN);
+      state,
+      lhs,
+      nil_exprt(),
+      rhs,
+      guard,
+      symex_targett::assignment_typet::HIDDEN);
     state.record_events=record_events;
   }
 
@@ -122,6 +127,11 @@ void goto_symext::symex_start_thread(statet &state)
 
     guardt guard;
     symex_assign_symbol(
-      state, lhs, nil_exprt(), rhs, guard, symex_targett::HIDDEN);
+      state,
+      lhs,
+      nil_exprt(),
+      rhs,
+      guard,
+      symex_targett::assignment_typet::HIDDEN);
   }
 }
diff --git a/src/goto-symex/symex_target.h b/src/goto-symex/symex_target.h
index e3b94fc15b6..eafea6d7e39 100644
--- a/src/goto-symex/symex_target.h
+++ b/src/goto-symex/symex_target.h
@@ -51,10 +51,15 @@ class symex_targett
     }
   };
 
-  typedef enum
+  enum class assignment_typet
   {
-    STATE, HIDDEN, VISIBLE_ACTUAL_PARAMETER, HIDDEN_ACTUAL_PARAMETER, PHI, GUARD
-  } assignment_typet;
+    STATE,
+    HIDDEN,
+    VISIBLE_ACTUAL_PARAMETER,
+    HIDDEN_ACTUAL_PARAMETER,
+    PHI,
+    GUARD,
+  };
 
   // read event
   virtual void shared_read(
diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp
index 3cf9612e556..5a4f5cd581e 100644
--- a/src/goto-symex/symex_target_equation.cpp
+++ b/src/goto-symex/symex_target_equation.cpp
@@ -250,8 +250,8 @@ void symex_target_equationt::assignment(
 
   SSA_step.cond_expr=equal_exprt(SSA_step.ssa_lhs, SSA_step.ssa_rhs);
   SSA_step.type=goto_trace_stept::ASSIGNMENT;
-  SSA_step.hidden=(assignment_type!=STATE &&
-                   assignment_type!=VISIBLE_ACTUAL_PARAMETER);
+  SSA_step.hidden=(assignment_type!=assignment_typet::STATE &&
+                   assignment_type!=assignment_typet::VISIBLE_ACTUAL_PARAMETER);
   SSA_step.source=source;
 
   merge_ireps(SSA_step);
@@ -286,7 +286,7 @@ void symex_target_equationt::decl(
   SSA_step.original_full_lhs=ssa_lhs.get_original_expr();
   SSA_step.type=goto_trace_stept::DECL;
   SSA_step.source=source;
-  SSA_step.hidden=(assignment_type!=STATE);
+  SSA_step.hidden=(assignment_type!=assignment_typet::STATE);
 
   // the condition is trivially true, and only
   // there so we see the symbols
@@ -1001,12 +1001,24 @@ void symex_target_equationt::SSA_stept::output(
     out << "ASSIGNMENT (";
     switch(assignment_type)
     {
-    case HIDDEN: out << "HIDDEN"; break;
-    case STATE: out << "STATE"; break;
-    case VISIBLE_ACTUAL_PARAMETER: out << "VISIBLE_ACTUAL_PARAMETER"; break;
-    case HIDDEN_ACTUAL_PARAMETER: out << "HIDDEN_ACTUAL_PARAMETER"; break;
-    case PHI: out << "PHI"; break;
-    case GUARD: out << "GUARD"; break;
+    case assignment_typet::HIDDEN:
+      out << "HIDDEN";
+      break;
+    case assignment_typet::STATE:
+      out << "STATE";
+      break;
+    case assignment_typet::VISIBLE_ACTUAL_PARAMETER:
+      out << "VISIBLE_ACTUAL_PARAMETER";
+      break;
+    case assignment_typet::HIDDEN_ACTUAL_PARAMETER:
+      out << "HIDDEN_ACTUAL_PARAMETER";
+      break;
+    case assignment_typet::PHI:
+      out << "PHI";
+      break;
+    case assignment_typet::GUARD:
+      out << "GUARD";
+      break;
     default:
       {
       }
diff --git a/src/goto-symex/symex_target_equation.h b/src/goto-symex/symex_target_equation.h
index 855b44ee0bb..845003e5cae 100644
--- a/src/goto-symex/symex_target_equation.h
+++ b/src/goto-symex/symex_target_equation.h
@@ -197,7 +197,7 @@ class symex_target_equationt:public symex_targett
     bool is_atomic_end() const      { return type==goto_trace_stept::ATOMIC_END; }
 
     // we may choose to hide
-    bool hidden;
+    bool hidden=false;
 
     exprt guard;
     literalt guard_literal;
@@ -206,7 +206,7 @@ class symex_target_equationt:public symex_targett
     ssa_exprt ssa_lhs;
     exprt ssa_full_lhs, original_full_lhs;
     exprt ssa_rhs;
-    assignment_typet assignment_type;
+    assignment_typet assignment_type=assignment_typet::STATE;
 
     // for ASSUME/ASSERT/GOTO/CONSTRAINT
     exprt cond_expr;
@@ -215,7 +215,7 @@ class symex_target_equationt:public symex_targett
 
     // for INPUT/OUTPUT
     irep_idt format_string, io_id;
-    bool formatted;
+    bool formatted=false;
     std::list<exprt> io_args;
     std::list<exprt> converted_io_args;
 
@@ -223,10 +223,10 @@ class symex_target_equationt:public symex_targett
     irep_idt identifier;
 
     // for SHARED_READ/SHARED_WRITE and ATOMIC_BEGIN/ATOMIC_END
-    unsigned atomic_section_id;
+    unsigned atomic_section_id=0;
 
     // for slicing
-    bool ignore;
+    bool ignore=false;
 
     SSA_stept():
       type(goto_trace_stept::NONE),