Pass original guard to apply_goto_condition

This is in preparation for calling try_filter_value_sets inside
apply_goto_condition

Author: Owen

src/goto-symex/goto_symex.h

@@ -322,12 +322,14 @@ class goto_symext
   /// \param current_state: state prior to the GOTO instruction
   /// \param jump_taken_state: state following taking the GOTO
   /// \param jump_not_taken_state: fall-through state
+  /// \param original_guard: the original GOTO condition
   /// \param new_guard: GOTO condition, L2 renamed and simplified
   /// \param ns: global namespace
   void apply_goto_condition(
     goto_symex_statet &current_state,
     goto_statet &jump_taken_state,
     goto_statet &jump_not_taken_state,
+    const exprt &original_guard,
     const exprt &new_guard,
     const namespacet &ns);
 

src/goto-symex/symex_goto.cpp

@@ -26,6 +26,7 @@ void goto_symext::apply_goto_condition(
   goto_symex_statet &current_state,
   goto_statet &jump_taken_state,
   goto_statet &jump_not_taken_state,
+  const exprt &original_guard,
   const exprt &new_guard,
   const namespacet &ns)
 {
@@ -262,7 +263,13 @@ void goto_symext::symex_goto(statet &state)
       auto &taken_state = backward ? state : goto_state_list.back().second;
       auto &not_taken_state = backward ? goto_state_list.back().second : state;
 
-      apply_goto_condition(state, taken_state, not_taken_state, new_guard, ns);
+      apply_goto_condition(
+        state,
+        taken_state,
+        not_taken_state,
+        instruction.get_condition(),
+        new_guard,
+        ns);
     }
 
     // produce new guard symbol