Add function for reverting formula slicing

This functionality is necessary to use slicing symex_target_equationt
in combination with incremental unwinding.

Author: peterschrammel

src/goto-symex/slice.cpp

@@ -262,3 +262,11 @@ 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 &equation);
+
 // this simply slices away anything after the last assertion
 void simple_slice(symex_target_equationt &equation);