From 9606967a9cc5333ecdf23e5969e7c22e906f0a87 Mon Sep 17 00:00:00 2001
From: Lucas Cordeiro <lucasccordeiro@gmail.com>
Date: Tue, 9 May 2017 15:43:21 +0100
Subject: [PATCH 1/5] added support for array_set in the full-slice option

---
 regression/goto-instrument/chain.sh | 21 +++++++++++++--------
 src/goto-instrument/full_slicer.cpp |  4 ++++
 2 files changed, 17 insertions(+), 8 deletions(-)

diff --git a/regression/goto-instrument/chain.sh b/regression/goto-instrument/chain.sh
index 68f50b095bc..b51c916390c 100755
--- a/regression/goto-instrument/chain.sh
+++ b/regression/goto-instrument/chain.sh
@@ -12,15 +12,20 @@ name=${name%.c}
 
 args=${@:1:$#-1}
 
-$goto_cc -o $name.gb $name.c
+if [ -f $name.c ]
+then
+  $goto_cc -o $name.gb $name.c
 # $goto_instrument --show-goto-functions $name.gb
-$goto_instrument $args $name.gb ${name}-mod.gb
-if [ ! -e ${name}-mod.gb ] ; then
-  cp $name.gb ${name}-mod.gb
-elif echo "$args" | grep -q -- "--dump-c" ; then
-  mv ${name}-mod.gb ${name}-mod.c
-  $goto_cc ${name}-mod.c -o ${name}-mod.gb
-  rm ${name}-mod.c
+  $goto_instrument $args $name.gb ${name}-mod.gb
+  if [ ! -e ${name}-mod.gb ] ; then
+    cp $name.gb ${name}-mod.gb
+  elif echo "$args" | grep -q -- "--dump-c" ; then
+    mv ${name}-mod.gb ${name}-mod.c
+    $goto_cc ${name}-mod.c -o ${name}-mod.gb
+    rm ${name}-mod.c
+  fi
+else
+  $goto_instrument $args $name ${name}-mod.gb
 fi
 $goto_instrument --show-goto-functions ${name}-mod.gb
 $cbmc ${name}-mod.gb
diff --git a/src/goto-instrument/full_slicer.cpp b/src/goto-instrument/full_slicer.cpp
index ca8de0f2cf7..90273957282 100644
--- a/src/goto-instrument/full_slicer.cpp
+++ b/src/goto-instrument/full_slicer.cpp
@@ -39,6 +39,10 @@ void full_slicert::add_function_calls(
   queuet &queue,
   const goto_functionst &goto_functions)
 {
+  // do not retain calls of empty functions
+  if (node.PC->function.empty())
+   return;
+
   goto_functionst::function_mapt::const_iterator f_it=
     goto_functions.function_map.find(node.PC->function);
   assert(f_it!=goto_functions.function_map.end());

From 2fc22f438ebf24a2b61be64dad88c515f8ab5314 Mon Sep 17 00:00:00 2001
From: Lucas Cordeiro <lucasccordeiro@gmail.com>
Date: Tue, 9 May 2017 16:32:29 +0100
Subject: [PATCH 2/5] added test case into goto-instrument regression for
 checking array_set

---
 regression/goto-instrument/chain.sh             |   9 ++++-----
 regression/goto-instrument/slice24/test.desc    |   6 ++++++
 .../goto-instrument/slice24/testSlice.class     | Bin 0 -> 1047 bytes
 .../goto-instrument/slice24/testSlice.java      |  16 ++++++++++++++++
 src/goto-instrument/full_slicer.cpp             |   5 ++---
 5 files changed, 28 insertions(+), 8 deletions(-)
 create mode 100644 regression/goto-instrument/slice24/test.desc
 create mode 100644 regression/goto-instrument/slice24/testSlice.class
 create mode 100644 regression/goto-instrument/slice24/testSlice.java

diff --git a/regression/goto-instrument/chain.sh b/regression/goto-instrument/chain.sh
index b51c916390c..e3b4d607a4a 100755
--- a/regression/goto-instrument/chain.sh
+++ b/regression/goto-instrument/chain.sh
@@ -12,8 +12,7 @@ name=${name%.c}
 
 args=${@:1:$#-1}
 
-if [ -f $name.c ]
-then
+if [ -f $name.c ] ; then
   $goto_cc -o $name.gb $name.c
 # $goto_instrument --show-goto-functions $name.gb
   $goto_instrument $args $name.gb ${name}-mod.gb
@@ -24,9 +23,9 @@ then
     $goto_cc ${name}-mod.c -o ${name}-mod.gb
     rm ${name}-mod.c
   fi
-else
-  $goto_instrument $args $name ${name}-mod.gb
-fi
 $goto_instrument --show-goto-functions ${name}-mod.gb
 $cbmc ${name}-mod.gb
+else
+  $cbmc $name
+fi
 
diff --git a/regression/goto-instrument/slice24/test.desc b/regression/goto-instrument/slice24/test.desc
new file mode 100644
index 00000000000..be5f1d60ff9
--- /dev/null
+++ b/regression/goto-instrument/slice24/test.desc
@@ -0,0 +1,6 @@
+CORE
+testSlice.class
+--full-slice
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
diff --git a/regression/goto-instrument/slice24/testSlice.class b/regression/goto-instrument/slice24/testSlice.class
new file mode 100644
index 0000000000000000000000000000000000000000..57f219541be4b482ae7c3f632179682209376e88
GIT binary patch
literal 1047
zcmZuwT~8B16g|@}-FCaQe6(0WP!zSGf+BuW5iOc%P)w>u@o8xX94xzJcF=eKgpn5?
zeep$2#Au>V`rvOe#(OuVZJO?8&&)k@@11+k%>McJ?FWE4EIR1NSPEGjc5npaHjX;5
zFvi9)h6#q_3?~>)G87pm8KxLc**NXs45n?&2n<emVJNjxfgdiZ&|9m^nt)gpNR*VX
z%z{9?IQdw>DhD+wkX=^3yuY)xCiO#hriCp}`2s`5XUm)3OK+y``5QA8qm{og&w;%a
z<5geW^R^rQ$x^l6$m~>t9bJ{T73awq8JbF6Rpm72agjsb#Q+9voON*yvjT<I1~>Mr
zzNK}bU7W|PO9ByGV7SO|iQzKC6^5&rcTvK;K&rWwjcYCza9yCUm3w7vQ&tUW)1u1H
zJ?&ME)D*13CAm&2kWN;yJV{d7M5zr$A$b+vrQ+|@q;J%^lA4;=#OFHs2N9iA;j%PQ
z+U)*xMK^M#i3wgwUG_qfhpb22+fB;^Z5EeNCKnU51!UW*uhSvZ5!Ga<w5&C?qvFgC
zEzk+CVw`SOKix9XS76m?76%oMJmC;oqcjQ{d#3gvKC&YY5GEp$WI+K3X-=+U7%_T*
z-|^BX#C9<_@)dFG9n#-nJ>5gk&xjo$Hu1I#X?KzwpX?f+>U8C#PB${$jdVN7AqwxM
zFVj{m_Zo|Ookp7GJ!B=QTbq8OByLjYPvBsS)?UNK8}#A>GWbPu4wH8VslO<QTrQuZ
sr$7-SO-bh>?STG)>=*Ry!nWSSiho9|wdKCNoQgJf7x@qlMHP+y2gxPe6aWAK

literal 0
HcmV?d00001

diff --git a/regression/goto-instrument/slice24/testSlice.java b/regression/goto-instrument/slice24/testSlice.java
new file mode 100644
index 00000000000..b80de88e648
--- /dev/null
+++ b/regression/goto-instrument/slice24/testSlice.java
@@ -0,0 +1,16 @@
+public class testSlice
+{
+   public static void main(String[] args)
+   {
+      char c = 0;
+      assert Character.isDefined(c)==true;
+      assert Character.isDigit(c)==false;
+      assert Character.isJavaIdentifierStart(c)==false;
+      assert Character.isJavaIdentifierPart(c)==true;
+      assert Character.isLetter(c)==false;
+      assert Character.isLetterOrDigit(c)==false;
+      assert Character.isLowerCase(c)==false;
+      assert Character.isUpperCase(c)==false;
+      assert Character.toUpperCase(c)==Character.toLowerCase(c);
+   }
+}
diff --git a/src/goto-instrument/full_slicer.cpp b/src/goto-instrument/full_slicer.cpp
index 90273957282..e4deede6068 100644
--- a/src/goto-instrument/full_slicer.cpp
+++ b/src/goto-instrument/full_slicer.cpp
@@ -39,9 +39,8 @@ void full_slicert::add_function_calls(
   queuet &queue,
   const goto_functionst &goto_functions)
 {
-  // do not retain calls of empty functions
-  if (node.PC->function.empty())
-   return;
+  if(node.PC->code.is_nil())
+    return;
 
   goto_functionst::function_mapt::const_iterator f_it=
     goto_functions.function_map.find(node.PC->function);

From b823e0a043649a4889fde24aa9ede7ce9fe5b03a Mon Sep 17 00:00:00 2001
From: Lucas Cordeiro <lucasccordeiro@gmail.com>
Date: Fri, 12 May 2017 10:17:58 +0100
Subject: [PATCH 3/5] added function call to working queue in the full-slicer

Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com>
---
 src/goto-instrument/full_slicer.cpp | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/goto-instrument/full_slicer.cpp b/src/goto-instrument/full_slicer.cpp
index e4deede6068..f7485390dff 100644
--- a/src/goto-instrument/full_slicer.cpp
+++ b/src/goto-instrument/full_slicer.cpp
@@ -321,6 +321,8 @@ void full_slicert::operator()(
       const exprt &s=to_code_dead(e_it->first->code).symbol();
       decl_dead[to_symbol_expr(s).get_identifier()].push(e_it->second);
     }
+    else if(e_it->first->is_function_call())
+      add_to_queue(queue, e_it->second, e_it->first);
   }
 
   // compute program dependence graph (and post-dominators)

From 09df41499c5c37cd1033c440a5a8500d0a0a6b9b Mon Sep 17 00:00:00 2001
From: Lucas Cordeiro <lucasccordeiro@gmail.com>
Date: Mon, 15 May 2017 15:09:28 +0100
Subject: [PATCH 4/5] added new test cases related to function call

---
 regression/goto-instrument/slice05/main.c     |   2 +
 regression/goto-instrument/slice07/test.desc  |   6 +--
 regression/goto-instrument/slice18/test.desc  |   2 +-
 regression/goto-instrument/slice24/test.desc  |   2 +-
 .../goto-instrument/slice24/testSlice.class   | Bin 1047 -> 634 bytes
 .../goto-instrument/slice24/testSlice.java    |  41 ++++++++++++------
 regression/goto-instrument/slice25/main.c     |  22 ++++++++++
 regression/goto-instrument/slice25/test.desc  |   6 +++
 src/goto-instrument/full_slicer.cpp           |   4 +-
 9 files changed, 63 insertions(+), 22 deletions(-)
 create mode 100644 regression/goto-instrument/slice25/main.c
 create mode 100644 regression/goto-instrument/slice25/test.desc

diff --git a/regression/goto-instrument/slice05/main.c b/regression/goto-instrument/slice05/main.c
index 30e59ce9c7e..79509173001 100644
--- a/regression/goto-instrument/slice05/main.c
+++ b/regression/goto-instrument/slice05/main.c
@@ -1,3 +1,5 @@
+#include <assert.h>
+
 int main()
 {
   int x = 1; /* considering changing this line */
diff --git a/regression/goto-instrument/slice07/test.desc b/regression/goto-instrument/slice07/test.desc
index f40f8bd1c64..1a93a2ec1cd 100644
--- a/regression/goto-instrument/slice07/test.desc
+++ b/regression/goto-instrument/slice07/test.desc
@@ -1,8 +1,6 @@
 KNOWNBUG
 main.c
 --full-slice
-^EXIT=6$
+^EXIT=0$
 ^SIGNAL=0$
-^\-\-full\-slice does not support C/Pthreads yet$
---
-^warning: ignoring
+^VERIFICATION SUCCESSFUL$
diff --git a/regression/goto-instrument/slice18/test.desc b/regression/goto-instrument/slice18/test.desc
index 03cff4a4fac..3793f7374e1 100644
--- a/regression/goto-instrument/slice18/test.desc
+++ b/regression/goto-instrument/slice18/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --full-slice
 ^EXIT=0$
diff --git a/regression/goto-instrument/slice24/test.desc b/regression/goto-instrument/slice24/test.desc
index be5f1d60ff9..51d38accc89 100644
--- a/regression/goto-instrument/slice24/test.desc
+++ b/regression/goto-instrument/slice24/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 testSlice.class
 --full-slice
 ^EXIT=10$
diff --git a/regression/goto-instrument/slice24/testSlice.class b/regression/goto-instrument/slice24/testSlice.class
index 57f219541be4b482ae7c3f632179682209376e88..d37e727d3e935d706837375fa332a77396021d9d 100644
GIT binary patch
literal 634
zcmYLGNl)8g5Pjn;PK*IV+B6M>eF;#3SZ+lK#3CUDI0RKHh=b#NppP1-vYq}IE*yI<
zNFWsn?);{zV#b2x;5Xx$_r2L({{MXfu!b)dY?Mt5Suju*7#67HVPQnPQ4?bpa>5z6
zFo8)EQ-s2l8$~LNbt{N=bmTUC)g;gfA-k>v9d8g))wyqk^mePM2>mr3sKfSELxsme
z=ERk&146NSTDx?Axl6tqTrAb&PzM)Z<za6<cD)}5?$3nJ4H9zep8qCp)m!b*Q+ryZ
z`eGHubzggGQKW42!{GuFwJ{CH#*9EO`fSXiN+@+JZoQAO8-}frknd=jn6ojD1%lJ1
zA2lwO7ZZ&0Wq}oe)nwLv9<s~Z_IW=%T~kFmRLxEm9x85gf|qlGao(}bS0JY(&9RpP
ztH5C#;J*r6Vw;(N0R0gn1{t$Su!uYg_`tqU&-hXX+u27L-ye{wE!-o`U*;CsYZTZs
z(>LgOM2@rhXAv_Ju_7|;m-)a$+{-Z6uJE=-@R6fA&_B$WD6;pd)74s19vB$3?$LA2
a!oQJD-67i*eeY02GBE5-nWL1{{QL^ZA#l3@

literal 1047
zcmZuwT~8B16g|@}-FCaQe6(0WP!zSGf+BuW5iOc%P)w>u@o8xX94xzJcF=eKgpn5?
zeep$2#Au>V`rvOe#(OuVZJO?8&&)k@@11+k%>McJ?FWE4EIR1NSPEGjc5npaHjX;5
zFvi9)h6#q_3?~>)G87pm8KxLc**NXs45n?&2n<emVJNjxfgdiZ&|9m^nt)gpNR*VX
z%z{9?IQdw>DhD+wkX=^3yuY)xCiO#hriCp}`2s`5XUm)3OK+y``5QA8qm{og&w;%a
z<5geW^R^rQ$x^l6$m~>t9bJ{T73awq8JbF6Rpm72agjsb#Q+9voON*yvjT<I1~>Mr
zzNK}bU7W|PO9ByGV7SO|iQzKC6^5&rcTvK;K&rWwjcYCza9yCUm3w7vQ&tUW)1u1H
zJ?&ME)D*13CAm&2kWN;yJV{d7M5zr$A$b+vrQ+|@q;J%^lA4;=#OFHs2N9iA;j%PQ
z+U)*xMK^M#i3wgwUG_qfhpb22+fB;^Z5EeNCKnU51!UW*uhSvZ5!Ga<w5&C?qvFgC
zEzk+CVw`SOKix9XS76m?76%oMJmC;oqcjQ{d#3gvKC&YY5GEp$WI+K3X-=+U7%_T*
z-|^BX#C9<_@)dFG9n#-nJ>5gk&xjo$Hu1I#X?KzwpX?f+>U8C#PB${$jdVN7AqwxM
zFVj{m_Zo|Ookp7GJ!B=QTbq8OByLjYPvBsS)?UNK8}#A>GWbPu4wH8VslO<QTrQuZ
sr$7-SO-bh>?STG)>=*Ry!nWSSiho9|wdKCNoQgJf7x@qlMHP+y2gxPe6aWAK

diff --git a/regression/goto-instrument/slice24/testSlice.java b/regression/goto-instrument/slice24/testSlice.java
index b80de88e648..7969f3f5ad1 100644
--- a/regression/goto-instrument/slice24/testSlice.java
+++ b/regression/goto-instrument/slice24/testSlice.java
@@ -1,16 +1,31 @@
+class test
+{
+  public void f1()
+  {
+    int y=0;
+    y++;
+  }
+
+  public void f2()
+  {
+    i++;
+  }
+
+  public int f3()
+  {
+    return i;
+  }
+
+  private int i;
+}
+
 public class testSlice
 {
-   public static void main(String[] args)
-   {
-      char c = 0;
-      assert Character.isDefined(c)==true;
-      assert Character.isDigit(c)==false;
-      assert Character.isJavaIdentifierStart(c)==false;
-      assert Character.isJavaIdentifierPart(c)==true;
-      assert Character.isLetter(c)==false;
-      assert Character.isLetterOrDigit(c)==false;
-      assert Character.isLowerCase(c)==false;
-      assert Character.isUpperCase(c)==false;
-      assert Character.toUpperCase(c)==Character.toLowerCase(c);
-   }
+  public static void main(String[] args)
+  {
+    test t = new test();
+    t.f1();
+    t.f2();
+    assert t.f3()==1;
+  }
 }
diff --git a/regression/goto-instrument/slice25/main.c b/regression/goto-instrument/slice25/main.c
new file mode 100644
index 00000000000..9282c5d1b28
--- /dev/null
+++ b/regression/goto-instrument/slice25/main.c
@@ -0,0 +1,22 @@
+#include <assert.h>
+
+int x;
+
+void f1()
+{
+  int y=0;
+  y++;
+}
+
+void f2()
+{
+  x++;
+}
+
+int main()
+{
+  f1();
+  f2();
+  assert(x==1);
+  return 0;
+}
diff --git a/regression/goto-instrument/slice25/test.desc b/regression/goto-instrument/slice25/test.desc
new file mode 100644
index 00000000000..bb36f86ad95
--- /dev/null
+++ b/regression/goto-instrument/slice25/test.desc
@@ -0,0 +1,6 @@
+CORE
+main.c
+--full-slice
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
diff --git a/src/goto-instrument/full_slicer.cpp b/src/goto-instrument/full_slicer.cpp
index f7485390dff..618971fda23 100644
--- a/src/goto-instrument/full_slicer.cpp
+++ b/src/goto-instrument/full_slicer.cpp
@@ -17,6 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-programs/remove_skip.h>
 
 #include "full_slicer_class.h"
+#include <iostream>
 
 void full_slicert::add_dependencies(
   const cfgt::nodet &node,
@@ -39,9 +40,6 @@ void full_slicert::add_function_calls(
   queuet &queue,
   const goto_functionst &goto_functions)
 {
-  if(node.PC->code.is_nil())
-    return;
-
   goto_functionst::function_mapt::const_iterator f_it=
     goto_functions.function_map.find(node.PC->function);
   assert(f_it!=goto_functions.function_map.end());

From 4b1c20b2f5fe52302c329fb9d7a85026dfc17dc6 Mon Sep 17 00:00:00 2001
From: Lucas Cordeiro <lucasccordeiro@gmail.com>
Date: Mon, 15 May 2017 15:15:11 +0100
Subject: [PATCH 5/5] combined full-slice with reachability-slice

---
 regression/cbmc-java/slice1/test.desc         |   6 +++++
 .../slice1}/testSlice.class                   | Bin
 .../slice1}/testSlice.java                    |   0
 regression/goto-instrument/chain.sh           |  22 +++++++----------
 .../{slice25 => slice24}/main.c               |   0
 regression/goto-instrument/slice24/test.desc  |   8 +++---
 regression/goto-instrument/slice25/test.desc  |   6 -----
 src/cbmc/Makefile                             |   1 +
 src/cbmc/cbmc_parse_options.cpp               |  14 +++++++++++
 src/goto-instrument/full_slicer.cpp           |   1 -
 .../goto_instrument_parse_options.cpp         |  23 ++++++++++--------
 11 files changed, 47 insertions(+), 34 deletions(-)
 create mode 100644 regression/cbmc-java/slice1/test.desc
 rename regression/{goto-instrument/slice24 => cbmc-java/slice1}/testSlice.class (100%)
 rename regression/{goto-instrument/slice24 => cbmc-java/slice1}/testSlice.java (100%)
 rename regression/goto-instrument/{slice25 => slice24}/main.c (100%)
 delete mode 100644 regression/goto-instrument/slice25/test.desc

diff --git a/regression/cbmc-java/slice1/test.desc b/regression/cbmc-java/slice1/test.desc
new file mode 100644
index 00000000000..51d38accc89
--- /dev/null
+++ b/regression/cbmc-java/slice1/test.desc
@@ -0,0 +1,6 @@
+KNOWNBUG
+testSlice.class
+--full-slice
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
diff --git a/regression/goto-instrument/slice24/testSlice.class b/regression/cbmc-java/slice1/testSlice.class
similarity index 100%
rename from regression/goto-instrument/slice24/testSlice.class
rename to regression/cbmc-java/slice1/testSlice.class
diff --git a/regression/goto-instrument/slice24/testSlice.java b/regression/cbmc-java/slice1/testSlice.java
similarity index 100%
rename from regression/goto-instrument/slice24/testSlice.java
rename to regression/cbmc-java/slice1/testSlice.java
diff --git a/regression/goto-instrument/chain.sh b/regression/goto-instrument/chain.sh
index e3b4d607a4a..68f50b095bc 100755
--- a/regression/goto-instrument/chain.sh
+++ b/regression/goto-instrument/chain.sh
@@ -12,20 +12,16 @@ name=${name%.c}
 
 args=${@:1:$#-1}
 
-if [ -f $name.c ] ; then
-  $goto_cc -o $name.gb $name.c
+$goto_cc -o $name.gb $name.c
 # $goto_instrument --show-goto-functions $name.gb
-  $goto_instrument $args $name.gb ${name}-mod.gb
-  if [ ! -e ${name}-mod.gb ] ; then
-    cp $name.gb ${name}-mod.gb
-  elif echo "$args" | grep -q -- "--dump-c" ; then
-    mv ${name}-mod.gb ${name}-mod.c
-    $goto_cc ${name}-mod.c -o ${name}-mod.gb
-    rm ${name}-mod.c
-  fi
+$goto_instrument $args $name.gb ${name}-mod.gb
+if [ ! -e ${name}-mod.gb ] ; then
+  cp $name.gb ${name}-mod.gb
+elif echo "$args" | grep -q -- "--dump-c" ; then
+  mv ${name}-mod.gb ${name}-mod.c
+  $goto_cc ${name}-mod.c -o ${name}-mod.gb
+  rm ${name}-mod.c
+fi
 $goto_instrument --show-goto-functions ${name}-mod.gb
 $cbmc ${name}-mod.gb
-else
-  $cbmc $name
-fi
 
diff --git a/regression/goto-instrument/slice25/main.c b/regression/goto-instrument/slice24/main.c
similarity index 100%
rename from regression/goto-instrument/slice25/main.c
rename to regression/goto-instrument/slice24/main.c
diff --git a/regression/goto-instrument/slice24/test.desc b/regression/goto-instrument/slice24/test.desc
index 51d38accc89..bb36f86ad95 100644
--- a/regression/goto-instrument/slice24/test.desc
+++ b/regression/goto-instrument/slice24/test.desc
@@ -1,6 +1,6 @@
-KNOWNBUG
-testSlice.class
+CORE
+main.c
 --full-slice
-^EXIT=10$
+^EXIT=0$
 ^SIGNAL=0$
-^VERIFICATION FAILED$
+^VERIFICATION SUCCESSFUL$
diff --git a/regression/goto-instrument/slice25/test.desc b/regression/goto-instrument/slice25/test.desc
deleted file mode 100644
index bb36f86ad95..00000000000
--- a/regression/goto-instrument/slice25/test.desc
+++ /dev/null
@@ -1,6 +0,0 @@
-CORE
-main.c
---full-slice
-^EXIT=0$
-^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
diff --git a/src/cbmc/Makefile b/src/cbmc/Makefile
index 4d890b0b5fa..5cc605b479f 100644
--- a/src/cbmc/Makefile
+++ b/src/cbmc/Makefile
@@ -32,6 +32,7 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../pointer-analysis/rewrite_index$(OBJEXT) \
       ../pointer-analysis/goto_program_dereference$(OBJEXT) \
       ../goto-instrument/full_slicer$(OBJEXT) \
+      ../goto-instrument/reachability_slicer$(OBJEXT) \
       ../goto-instrument/nondet_static$(OBJEXT) \
       ../goto-instrument/cover$(OBJEXT) \
       ../analyses/analyses$(LIBEXT) \
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index d2f1c178d8e..3e267e3ba38 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -50,6 +50,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-symex/adjust_float_expressions.h>
 
 #include <goto-instrument/full_slicer.h>
+#include <goto-instrument/reachability_slicer.h>
 #include <goto-instrument/nondet_static.h>
 #include <goto-instrument/cover.h>
 
@@ -821,6 +822,19 @@ bool cbmc_parse_optionst::process_goto_program(
     status() << "Generic Property Instrumentation" << eom;
     goto_check(ns, options, goto_functions);
 
+    // full slice?
+    if(cmdline.isset("full-slice"))
+    {
+      status() << "Performing a full slice" << eom;
+      full_slicer(goto_functions, ns);
+
+      status() << "Performing a reachability slice" << eom;
+       if(cmdline.isset("property"))
+         reachability_slicer(goto_functions, cmdline.get_values("property"));
+       else
+         reachability_slicer(goto_functions);
+    }
+
     // checks don't know about adjusted float expressions
     adjust_float_expressions(goto_functions, ns);
 
diff --git a/src/goto-instrument/full_slicer.cpp b/src/goto-instrument/full_slicer.cpp
index 618971fda23..9f55c39f701 100644
--- a/src/goto-instrument/full_slicer.cpp
+++ b/src/goto-instrument/full_slicer.cpp
@@ -17,7 +17,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-programs/remove_skip.h>
 
 #include "full_slicer_class.h"
-#include <iostream>
 
 void full_slicert::add_dependencies(
   const cfgt::nodet &node,
diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
index b807b21dc9a..c2599c1ce83 100644
--- a/src/goto-instrument/goto_instrument_parse_options.cpp
+++ b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -1410,16 +1410,6 @@ void goto_instrument_parse_optionst::instrument_goto_program()
     nondet_volatile(symbol_table, goto_functions);
   }
 
-  // reachability slice?
-  if(cmdline.isset("reachability-slice"))
-  {
-    status() << "Performing a reachability slice" << eom;
-    if(cmdline.isset("property"))
-      reachability_slicer(goto_functions, cmdline.get_values("property"));
-    else
-      reachability_slicer(goto_functions);
-  }
-
   // full slice?
   if(cmdline.isset("full-slice"))
   {
@@ -1433,6 +1423,19 @@ void goto_instrument_parse_optionst::instrument_goto_program()
       full_slicer(goto_functions, ns);
   }
 
+  // reachability slice?
+  if(cmdline.isset("reachability-slice") || cmdline.isset("full-slice"))
+  {
+    status() << "Performing a reachability slice" << eom;
+    if(cmdline.isset("property"))
+      reachability_slicer(goto_functions, cmdline.get_values("property"));
+    else
+      reachability_slicer(goto_functions);
+  }
+
+  // label the assertions
+  label_properties(goto_functions);
+
   // recalculate numbers, etc.
   goto_functions.update();
 }