diff --git a/src/goto-symex/slice.cpp b/src/goto-symex/slice.cpp
index 5da99ac49b0..565f9e1b24b 100644
--- a/src/goto-symex/slice.cpp
+++ b/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;
+  }
+}
diff --git a/src/goto-symex/slice.h b/src/goto-symex/slice.h
index 5d62bd5d92a..ae906e5518e 100644
--- a/src/goto-symex/slice.h
+++ b/src/goto-symex/slice.h
@@ -19,6 +19,9 @@ Author: Daniel Kroening, kroening@kroening.com
 // 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);