diff --git a/regression/goto-instrument-unwind/Makefile b/regression/goto-instrument-unwind/Makefile
new file mode 100644
index 00000000000..45c2db4d8c2
--- /dev/null
+++ b/regression/goto-instrument-unwind/Makefile
@@ -0,0 +1,33 @@
+default: tests.log
+
+testalpha:
+	@../test.pl -c ../unwind-chain.sh -C
+
+testbeta:
+	@../test.pl -c ../unwind-chain.sh -T
+
+testimpr:
+	@../test.pl -c ../unwind-chain.sh -K
+
+testnew:
+	@../test.pl -c ../unwind-chain.sh -F
+
+test:
+	@../test.pl -c ../unwind-chain.sh 
+
+tests.log: ../test.pl
+	@../test.pl -c ../unwind-chain.sh 
+
+clean:
+	@for dir in *; do \
+                if [ -d "$$dir" ]; then \
+                        rm $$dir/*.txt $$dir/*.dot $$dir/*.gb $$dir/*.out; \
+                fi; \
+        done;
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.c" "$$dir/*.out"; \
+		fi; \
+	done;
diff --git a/regression/goto-instrument-unwind/break-loop1/main.c b/regression/goto-instrument-unwind/break-loop1/main.c
new file mode 100644
index 00000000000..b5323c4ff5d
--- /dev/null
+++ b/regression/goto-instrument-unwind/break-loop1/main.c
@@ -0,0 +1,30 @@
+
+void f() {}
+
+int main()
+{
+  /**
+   * This is a test case for the unwind operation of goto-instrument;
+   * every loop will be unwound K times
+   **/
+  const unsigned K=10;
+  
+  const unsigned n=100;
+  unsigned c=0, i;
+  unsigned tres=K/2;;
+
+  for(i=1; i<=n; i++)
+  {
+    f();
+    c++;
+    if(i==tres)
+      break;
+  }
+
+  unsigned eva=n;
+  if(K<eva) eva=K;
+  if(tres<eva) eva=tres;
+  
+  __CPROVER_assert(c==eva, "break a loop unwind (1)");
+
+}
diff --git a/regression/goto-instrument-unwind/break-loop1/test.desc b/regression/goto-instrument-unwind/break-loop1/test.desc
new file mode 100644
index 00000000000..6d9a8177c73
--- /dev/null
+++ b/regression/goto-instrument-unwind/break-loop1/test.desc
@@ -0,0 +1,7 @@
+CORE
+main.c
+10
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/goto-instrument-unwind/break-loop2/main.c b/regression/goto-instrument-unwind/break-loop2/main.c
new file mode 100644
index 00000000000..86950abd484
--- /dev/null
+++ b/regression/goto-instrument-unwind/break-loop2/main.c
@@ -0,0 +1,30 @@
+
+void f() {}
+
+int main()
+{
+  /**
+   * This is a test case for the unwind operation of goto-instrument;
+   * every loop will be unwound K times
+   **/
+  const unsigned K=100;
+  
+  const unsigned n=10;
+  unsigned c=0, i;
+  unsigned tres=K/2;;
+
+  for(i=1; i<=n; i++)
+  {
+    f();
+    c++;
+    if(i==tres)
+      break;
+  }
+
+  unsigned eva=n;
+  if(K<eva) eva=K;
+  if(tres<eva) eva=tres;
+  
+  __CPROVER_assert(c==eva, "break a loop unwind (2)");
+
+}
diff --git a/regression/goto-instrument-unwind/break-loop2/test.desc b/regression/goto-instrument-unwind/break-loop2/test.desc
new file mode 100644
index 00000000000..7639d204406
--- /dev/null
+++ b/regression/goto-instrument-unwind/break-loop2/test.desc
@@ -0,0 +1,7 @@
+CORE
+main.c
+100
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/goto-instrument-unwind/continue-loop1/main.c b/regression/goto-instrument-unwind/continue-loop1/main.c
new file mode 100644
index 00000000000..1be574b0dc1
--- /dev/null
+++ b/regression/goto-instrument-unwind/continue-loop1/main.c
@@ -0,0 +1,30 @@
+
+void f() {}
+
+int main()
+{
+  /**
+   * This is a test case for the unwind operation of goto-instrument;
+   * every loop will be unwound K times
+   **/
+  const unsigned K=10;
+  
+  const unsigned n=100;
+  unsigned c=0, i;
+  unsigned tres=K/2;;
+
+  for(i=1; i<=n; i++)
+  {
+    f();
+    if(i>tres)
+      continue;
+    c++;
+  }
+
+  unsigned eva=n;
+  if(K<eva) eva=K;
+  if(tres<eva) eva=tres;
+  
+  __CPROVER_assert(c==eva, "continue in a loop unwind (1)");
+
+}
diff --git a/regression/goto-instrument-unwind/continue-loop1/test.desc b/regression/goto-instrument-unwind/continue-loop1/test.desc
new file mode 100644
index 00000000000..6d9a8177c73
--- /dev/null
+++ b/regression/goto-instrument-unwind/continue-loop1/test.desc
@@ -0,0 +1,7 @@
+CORE
+main.c
+10
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/goto-instrument-unwind/continue-loop2/main.c b/regression/goto-instrument-unwind/continue-loop2/main.c
new file mode 100644
index 00000000000..6df9b7cb9fb
--- /dev/null
+++ b/regression/goto-instrument-unwind/continue-loop2/main.c
@@ -0,0 +1,30 @@
+
+void f() {}
+
+int main()
+{
+  /**
+   * This is a test case for the unwind operation of goto-instrument;
+   * every loop will be unwound K times
+   **/
+  const unsigned K=100;
+  
+  const unsigned n=10;
+  unsigned c=0, i;
+  unsigned tres=n/2;;
+
+  for(i=1; i<=n; i++)
+  {
+    f();
+    if(i>tres)
+      continue;
+    c++;
+  }
+
+  unsigned eva=n;
+  if(K<eva) eva=K;
+  if(tres<eva) eva=tres;
+  
+  __CPROVER_assert(c==eva, "continue in a loop unwind (2)");
+
+}
diff --git a/regression/goto-instrument-unwind/continue-loop2/test.desc b/regression/goto-instrument-unwind/continue-loop2/test.desc
new file mode 100644
index 00000000000..7639d204406
--- /dev/null
+++ b/regression/goto-instrument-unwind/continue-loop2/test.desc
@@ -0,0 +1,7 @@
+CORE
+main.c
+100
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/goto-instrument-unwind/empty-loop1/main.c b/regression/goto-instrument-unwind/empty-loop1/main.c
new file mode 100644
index 00000000000..9108875e81f
--- /dev/null
+++ b/regression/goto-instrument-unwind/empty-loop1/main.c
@@ -0,0 +1,22 @@
+
+int main()
+{
+  /**
+   * This is a test case for the unwind operation of goto-instrument;
+   * every loop will be unwound K times
+   **/
+  const unsigned K=10;
+  
+  const unsigned n=100;
+  unsigned i=0;
+
+  while(++i<n)
+  {
+  }
+
+  unsigned eva=n;
+  if(K<eva) eva=K;
+  
+  __CPROVER_assert(i==eva, "Empty loop unwind (1)");
+
+}
diff --git a/regression/goto-instrument-unwind/empty-loop1/test.desc b/regression/goto-instrument-unwind/empty-loop1/test.desc
new file mode 100644
index 00000000000..6d9a8177c73
--- /dev/null
+++ b/regression/goto-instrument-unwind/empty-loop1/test.desc
@@ -0,0 +1,7 @@
+CORE
+main.c
+10
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/goto-instrument-unwind/empty-loop2/main.c b/regression/goto-instrument-unwind/empty-loop2/main.c
new file mode 100644
index 00000000000..504f840a4dc
--- /dev/null
+++ b/regression/goto-instrument-unwind/empty-loop2/main.c
@@ -0,0 +1,22 @@
+
+int main()
+{
+  /**
+   * This is a test case for the unwind operation of goto-instrument;
+   * every loop will be unwound K times
+   **/
+  const unsigned K=100;
+  
+  const unsigned n=10;
+  unsigned i=0;
+
+  while(++i<n)
+  {
+  }
+
+  unsigned eva=n;
+  if(K<eva) eva=K;
+  
+  __CPROVER_assert(i==eva, "Empty loop unwind (1)");
+
+}
diff --git a/regression/goto-instrument-unwind/empty-loop2/test.desc b/regression/goto-instrument-unwind/empty-loop2/test.desc
new file mode 100644
index 00000000000..7639d204406
--- /dev/null
+++ b/regression/goto-instrument-unwind/empty-loop2/test.desc
@@ -0,0 +1,7 @@
+CORE
+main.c
+100
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/goto-instrument-unwind/nested-loops1/main.c b/regression/goto-instrument-unwind/nested-loops1/main.c
new file mode 100644
index 00000000000..a59ab146a47
--- /dev/null
+++ b/regression/goto-instrument-unwind/nested-loops1/main.c
@@ -0,0 +1,40 @@
+
+void f() {}
+void f2() {}
+
+int main()
+{
+  /**
+   * This is a test case for the unwind operation of goto-instrument;
+   * every loop will be unwound K times
+   **/
+  const unsigned K=10;
+  
+  const unsigned n=100;
+  unsigned c=0, i;
+
+  for(i=1; i<=n; i++)
+  {
+    f();
+    c++;
+
+    // the nested loop
+    unsigned j, c2=0;
+    for(j=1; j<=i; j++)
+    {
+      f2();
+      c2++;
+    }
+    unsigned eva2=i;
+    if(K<eva2) eva2=K;
+    
+    __CPROVER_assert(c2==eva2, "Nested loops unwind (1): the inner one");
+
+  }
+
+  unsigned eva=n;
+  if(K<eva) eva=K;
+  
+  __CPROVER_assert(c==eva, "Nested loops unwind (1)");
+
+}
diff --git a/regression/goto-instrument-unwind/nested-loops1/test.desc b/regression/goto-instrument-unwind/nested-loops1/test.desc
new file mode 100644
index 00000000000..6d9a8177c73
--- /dev/null
+++ b/regression/goto-instrument-unwind/nested-loops1/test.desc
@@ -0,0 +1,7 @@
+CORE
+main.c
+10
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/goto-instrument-unwind/nested-loops2/main.c b/regression/goto-instrument-unwind/nested-loops2/main.c
new file mode 100644
index 00000000000..debeca41144
--- /dev/null
+++ b/regression/goto-instrument-unwind/nested-loops2/main.c
@@ -0,0 +1,40 @@
+
+void f() {}
+void f2() {}
+
+int main()
+{
+  /**
+   * This is a test case for the unwind operation of goto-instrument;
+   * every loop will be unwound K times
+   **/
+  const unsigned K=10;
+  
+  const unsigned n=6;
+  unsigned c=0, i;
+
+  for(i=1; i<=n; i++)
+  {
+    f();
+    c++;
+
+    // the nested loop
+    unsigned j, c2=0;
+    for(j=1; j<=i; j++)
+    {
+      f2();
+      c2++;
+    }
+    unsigned eva2=i;
+    if(K<eva2) eva2=K;
+    
+    __CPROVER_assert(c2==eva2, "Nested loops unwind (2): the inner one");
+
+  }
+
+  unsigned eva=n;
+  if(K<eva) eva=K;
+  
+  __CPROVER_assert(c==eva, "Nested loops unwind (2)");
+
+}
diff --git a/regression/goto-instrument-unwind/nested-loops2/test.desc b/regression/goto-instrument-unwind/nested-loops2/test.desc
new file mode 100644
index 00000000000..6d9a8177c73
--- /dev/null
+++ b/regression/goto-instrument-unwind/nested-loops2/test.desc
@@ -0,0 +1,7 @@
+CORE
+main.c
+10
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/goto-instrument-unwind/simple-loop1/main.c b/regression/goto-instrument-unwind/simple-loop1/main.c
new file mode 100644
index 00000000000..65bfa80ac48
--- /dev/null
+++ b/regression/goto-instrument-unwind/simple-loop1/main.c
@@ -0,0 +1,26 @@
+
+void f() {}
+
+int main()
+{
+  /**
+   * This is a test case for the unwind operation of goto-instrument;
+   * every loop will be unwound K times
+   **/
+  const unsigned K=10;
+  
+  const unsigned n=100;
+  unsigned c=0, i;
+
+  for(i=1; i<=n; i++)
+  {
+    f();
+    c++;
+  }
+
+  unsigned eva=n;
+  if(K<eva) eva=K;
+  
+  __CPROVER_assert(c==eva, "Simple loop unwind (1)");
+
+}
diff --git a/regression/goto-instrument-unwind/simple-loop1/test.desc b/regression/goto-instrument-unwind/simple-loop1/test.desc
new file mode 100644
index 00000000000..6d9a8177c73
--- /dev/null
+++ b/regression/goto-instrument-unwind/simple-loop1/test.desc
@@ -0,0 +1,7 @@
+CORE
+main.c
+10
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/goto-instrument-unwind/simple-loop2/main.c b/regression/goto-instrument-unwind/simple-loop2/main.c
new file mode 100644
index 00000000000..b76d9f6c8a1
--- /dev/null
+++ b/regression/goto-instrument-unwind/simple-loop2/main.c
@@ -0,0 +1,26 @@
+
+void f() {}
+
+int main()
+{
+  /**
+   * This is a test case for the unwind operation of goto-instrument;
+   * every loop will be unwound K times
+   **/
+  const unsigned K=100;
+  
+  const unsigned n=10;
+  unsigned c=0, i;
+
+  for(i=1; i<=n; i++)
+  {
+    f();
+    c++;
+  }
+
+  unsigned eva=n;
+  if(K<eva) eva=K;
+  
+  __CPROVER_assert(c==eva, "Simple loop unwind (1)");
+
+}
diff --git a/regression/goto-instrument-unwind/simple-loop2/test.desc b/regression/goto-instrument-unwind/simple-loop2/test.desc
new file mode 100644
index 00000000000..7639d204406
--- /dev/null
+++ b/regression/goto-instrument-unwind/simple-loop2/test.desc
@@ -0,0 +1,7 @@
+CORE
+main.c
+100
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/goto-instrument-unwind/unwind-chain.sh b/regression/goto-instrument-unwind/unwind-chain.sh
new file mode 100755
index 00000000000..95348ef89c0
--- /dev/null
+++ b/regression/goto-instrument-unwind/unwind-chain.sh
@@ -0,0 +1,27 @@
+#!/bin/bash
+
+src=../../../src
+goto_cc=$src/goto-cc/goto-cc
+goto_instrument=$src/goto-instrument/goto-instrument
+cbmc=$src/cbmc/cbmc
+
+function usage() {
+  echo "Usage: chain unwind-num test_file.c"
+  exit 1
+}
+
+echo "Usage: process test_file.c to goto program"
+
+if [ $# -eq 2 ]
+then
+  unwind_num=$1
+  name=`echo $2 | cut -d. -f1`
+  echo $unwind_num
+  echo $name
+else
+  usage
+fi
+
+$goto_cc -o $name.gb $name.c
+$goto_instrument  $name.gb ${name}-unwound.gb --unwind $unwind_num
+$cbmc ${name}-unwound.gb
diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
index 4e04cf172ab..3304c2529b7 100644
--- a/src/goto-instrument/goto_instrument_parse_options.cpp
+++ b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -83,6 +83,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "thread_instrumentation.h"
 #include "skip_loops.h"
 #include "code_contracts.h"
+#include "unwind.h"
+
+
 
 /*******************************************************************\
 
@@ -144,6 +147,17 @@ int goto_instrument_parse_optionst::doit()
     get_goto_program();
     instrument_goto_program();
 
+    if(cmdline.isset("unwind"))
+    {
+
+      int k = stoi(cmdline.get_value("unwind"));
+
+      goto_unwind(goto_functions, k);
+
+      goto_functions.update();
+      goto_functions.compute_loop_numbers();
+    }
+
     if(cmdline.isset("show-value-sets"))
     {
       do_function_pointer_removal();
diff --git a/src/goto-instrument/unwind.cpp b/src/goto-instrument/unwind.cpp
index e8b9c1d0ed0..8720d0af788 100644
--- a/src/goto-instrument/unwind.cpp
+++ b/src/goto-instrument/unwind.cpp
@@ -7,8 +7,9 @@ Author: Daniel Kroening, kroening@kroening.com
 \*******************************************************************/
 
 #include <util/std_expr.h>
-
+#include <goto-programs/goto_functions.h>
 #include "unwind.h"
+#include "loop_utils.h"
 
 /*******************************************************************\
 
@@ -170,3 +171,61 @@ void unwind(
   // update it all
   goto_program.update();
 }
+
+/*******************************************************************\
+
+Function: goto_unwind
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void goto_unwind(
+  goto_functionst &goto_functions,
+  const unsigned k)
+{
+  // Here we unwind all loops in the program.
+  // Each loop body is simply repeated k times (if condition holds) 
+  Forall_goto_functions(it, goto_functions)
+  {
+    goto_functionst::goto_functiont &goto_function=it->second;
+    if(!goto_function.body_available())
+    {
+      continue;
+    }
+    goto_programt &goto_program=goto_function.body;
+
+    // the unwinding continues until there is no loop in the function
+    while(true)
+    {
+      natural_loops_mutablet natural_loops(goto_program);
+      // if there is no loop anymore in the current function,
+      // then go to the next function for unwinding
+      if(natural_loops.loop_map.size()==0)
+      {
+        break;
+      }
+      typedef const natural_loops_mutablet::natural_loopt loopt;
+      for(natural_loops_mutablet::loop_mapt::const_iterator
+          l_it=natural_loops.loop_map.begin();
+          l_it!=natural_loops.loop_map.end();
+          l_it++)
+      {
+        // save a copy of the loop guard
+        const exprt loop_guard=l_it->first->guard;
+
+        const loopt &loop=l_it->second;
+        assert(!loop.empty());
+        goto_programt::targett loop_exit=get_loop_exit(loop);
+
+        unwind(goto_program, l_it->first, loop_exit, k);
+
+      }
+    }
+  }
+}
+
diff --git a/src/goto-instrument/unwind.h b/src/goto-instrument/unwind.h
index ae7fb8798f7..ac93496a842 100644
--- a/src/goto-instrument/unwind.h
+++ b/src/goto-instrument/unwind.h
@@ -24,4 +24,8 @@ void unwind(
   const unsigned k,
   std::vector<goto_programt::targett> &iteration_points);
 
+void goto_unwind(
+  goto_functionst &goto_functions,
+  const unsigned k);
+
 #endif