Add function for reverting formula slicing

This functionality is necessary to use slicing
of symex_target_equationt in combination with incremental
unwinding. Assertions in future unwindings may depend
on steps that have been sliced away in previous
unwindings. Thus, we have to undo and recompute the slice.

Author: peterschrammel

src/goto-symex/slice.cpp

@@ -262,3 +262,12 @@ void simple_slice(symex_target_equationt &equation)
       s_it->ignore=true;
   }
 }
+
+void revert_slice(symex_target_equationt &equation)
+{
+  // set ignore to false
+  for(auto step : equation.SSA_steps)
+  {
+    step.ignore = false;
+  }
+}

src/goto-symex/slice.h

@@ -19,6 +19,9 @@ Author: Daniel Kroening, [email protected]
 // slice an equation with respect to the assertions contained therein
 void slice(symex_target_equationt &equation);
 
+/// Undo whatever has been done by `slice`
+void revert_slice(symex_target_equationt &);
+
 // this simply slices away anything after the last assertion
 void simple_slice(symex_target_equationt &equation);