Regression test for constant propagator merge bug

Author: peterschrammel

regression/goto-instrument/constant-propagation1/main.c

@@ -0,0 +1,18 @@
+#include <assert.h>
+
+void main()
+{
+  unsigned char n;
+  __CPROVER_assume(n > 0);   // To keep division well defined
+  __CPROVER_assume(n * n > 0);   // To keep division well defined
+
+  unsigned char i = 0;
+  unsigned char j = 0;
+
+  unsigned char aux1 = i / (n * n);
+  for (i = 0; i < n; ++i, aux1 = i / (n * n)) {
+    for (j = 0; j < n; ++j) {
+    }
+  }
+  assert(i != n);
+}

regression/goto-instrument/constant-propagation1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--constant-propagator --unwind 3
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

src/analyses/constant_propagator.cpp

@@ -66,7 +66,9 @@ void constant_propagator_domaint::transform(
     dynamic_cast<constant_propagator_ait *>(&ai);
   bool have_dirty=(cp!=nullptr);
 
-  // INVARIANT(!values.is_bottom);
+  // Transform on a domain that is bottom is possible
+  // if a branch is impossible the target can still wind
+  // up on the work list.
   if(values.is_bottom)
     return;