Clean-up

This will be merged later if people agree with it / it fixes CI

Author: JohnDumbell

src/goto-symex/goto_state.h

@@ -74,13 +74,6 @@ class goto_statet
     : guard(true_exprt(), guard_manager)
   {
   }
-
-  void move_from(goto_statet &&other_state)
-  {
-    level2 = std::move(other_state.level2);
-    propagation = std::move(other_state.propagation);
-    value_set = std::move(other_state.value_set);
-  }
 };
 
 #endif // CPROVER_GOTO_SYMEX_GOTO_STATE_H

src/goto-symex/symex_goto.cpp

@@ -211,11 +211,13 @@ void goto_symext::symex_goto(statet &state)
   framet::goto_state_listt &goto_state_list =
     state.call_stack().top().goto_state_map[new_state_pc];
 
-  // On an unconditional GOTO we don't need our state any more, as it will be
-  // overwritten by merge_goto. Therefore we move it onto goto_state_list
-  // instead of copying as usual.
+  // On an unconditional GOTO we don't need our state, as it will be overwritten
+  // by merge_goto. Therefore we move it onto goto_state_list instead of copying
+  // as usual.
   if(new_guard.is_true())
   {
+    // The move here only moves goto_statet, the base class of goto_symex_statet
+    // and not the entire thing.
     goto_state_list.emplace_back(state.source, std::move(state));
 
     symex_transition(state, state_pc, backward);
@@ -330,7 +332,7 @@ void goto_symext::merge_goto(
   {
     if(state.guard.is_false())
     {
-      state.move_from(std::move(goto_state));
+      static_cast<goto_statet&>(state) = std::move(goto_state);
     }
     else
     {
@@ -339,14 +341,14 @@ void goto_symext::merge_goto(
 
       // merge value sets
       state.value_set.make_union(goto_state.value_set);
-    }
-  }
 
-  // adjust guard
-  state.guard|=goto_state.guard;
+      // adjust guard
+      state.guard|=goto_state.guard;
 
-  // adjust depth
-  state.depth=std::min(state.depth, goto_state.depth);
+      // adjust depth
+      state.depth=std::min(state.depth, goto_state.depth);
+    }
+  }
 }
 
 /// Applies f to `(k, ssa, i, j)` if the first map maps k to (ssa, i) and