Fix bug in constant propagator

Before it was using the index operator. However, since there is no
initialisation, this caused an error if there was unreachable code in
the goto model. This can be fixed by simply using abstract_state_before
which will always return a valid domain state (bottom for unreachable
code) instead.

Author: Hannes Steffenhagen

regression/goto-instrument/constant_propagator_unreachable/test.c

@@ -0,0 +1,12 @@
+#include <assert.h>
+
+void unreachable(void)
+{
+  int x = 0;
+  assert(x != 0);
+}
+
+int main(void)
+{
+  return 0;
+}

regression/goto-instrument/constant_propagator_unreachable/test.desc

@@ -0,0 +1,11 @@
+CORE
+test.c
+--constant-propagator
+^EXIT=0$
+^SIGNAL=0$
+VERIFICATION SUCCESSFUL
+--
+failed to find state
+--
+This is testing for a previous regression that caused constant propagation to
+fail in unreachable code

src/analyses/constant_propagator.cpp

@@ -751,8 +751,10 @@ void constant_propagator_ait::replace(
 {
   Forall_goto_program_instructions(it, goto_function.body)
   {
-    // Works because this is a location (but not history) sensitive domain
-    const constant_propagator_domaint &d = (*this)[it];
+    auto const current_domain_ptr =
+      std::dynamic_pointer_cast<const constant_propagator_domaint>(
+        this->abstract_state_before(it));
+    const constant_propagator_domaint &d = *current_domain_ptr;
 
     if(d.is_bottom())
       continue;