Throw error if reachability slicer has no slicing criteria

If no slicing criteria are found, the reachability slicer should throw an error.
Likely due to trying to slice something with no properties, or user specifying a
property with a typo in the name

Author: polgreen

regression/goto-instrument/slicing_criterion1/main.c

@@ -0,0 +1,8 @@
+void a()
+{
+}
+
+int main()
+{
+  a();
+}

regression/goto-instrument/slicing_criterion1/test.desc

@@ -0,0 +1,6 @@
+CORE
+main.c
+--reachability-slice
+^Reason: no slicing criterion found$
+^EXIT=1$
+^SIGNAL=0$

regression/goto-instrument/slicing_criterion2/main.c

@@ -0,0 +1,9 @@
+void a()
+{
+  __CPROVER_assert(0, "");
+}
+
+int main()
+{
+  a();
+}

regression/goto-instrument/slicing_criterion2/test.desc

@@ -0,0 +1,6 @@
+CORE
+main.c
+--reachability-slice --property property-name-with-typo
+^Reason: no slicing criterion found$
+^EXIT=1$
+^SIGNAL=0$

src/goto-instrument/reachability_slicer.cpp

@@ -22,7 +22,8 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/remove_skip.h>
 #include <goto-programs/remove_unreachable.h>
 
-#include "util/message.h"
+#include <util/exception_utils.h>
+#include <util/message.h>
 
 #include "full_slicer_class.h"
 #include "reachability_slicer_class.h"
@@ -46,6 +47,14 @@ reachability_slicert::get_sources(
       sources.push_back(e_it.second);
   }
 
+  if(sources.empty())
+  {
+    throw invalid_command_line_argument_exceptiont{
+      "no slicing criterion found",
+      "--property",
+      "provide at least one property using --property <property>"};
+  }
+
   return sources;
 }