Merge pull request #4064 from peterschrammel/undo-slice

Add function for reverting formula slicing

Author: tautschnig

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);