Prune TOP values when assuming less than expressions

Remove duplication in data_dependency & write_location
merge and meet. Correct data_dependency_contextt::
has_been_modified to verify child object is also unchanged

Author: jezhiggins

regression/goto-analyzer/pruning-gt/test-constants.desc

@@ -3,6 +3,5 @@ main.c
 --variable-sensitivity --vsd-values constants --verify
 ^EXIT=0$
 ^SIGNAL=0$
-\[main\.assertion\.1\] line .* assertion x > 10: UNKNOWN
-
+\[main\.assertion\.1\] line .* assertion x > 10: SUCCESS
 --

regression/goto-analyzer/pruning-lt-nondet-2/main.c

@@ -0,0 +1,9 @@
+int main()
+{
+  int x = nondet();
+
+  if(10 < x)
+  {
+    assert(5 < x);
+  }
+}

regression/goto-analyzer/pruning-lt-nondet-2/test-constants.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--variable-sensitivity --vsd-values constants --verify
+^EXIT=0$
+^SIGNAL=0$
+\[main\.assertion\.1\] line .* assertion 5 < x: SUCCESS
+--

regression/goto-analyzer/pruning-lt-nondet-2/test-intervals.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--variable-sensitivity --vsd-values intervals --verify
+^EXIT=0$
+^SIGNAL=0$
+\[main\.assertion\.1\] line .* assertion 5 < x: SUCCESS
+--

regression/goto-analyzer/pruning-lt-nondet-2/test-value-sets.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--variable-sensitivity --vsd-values set-of-constants --verify
+^EXIT=0$
+^SIGNAL=0$
+\[main\.assertion\.1\] line .* assertion 5 < x: SUCCESS
+--

regression/goto-analyzer/pruning-lt-nondet/main.c

@@ -0,0 +1,9 @@
+int main()
+{
+  int x = nondet();
+
+  if(x < 10)
+  {
+    assert(x < 20);
+  }
+}

regression/goto-analyzer/pruning-lt-nondet/test-constants.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--variable-sensitivity --vsd-values constants --verify
+^EXIT=0$
+^SIGNAL=0$
+\[main\.assertion\.1\] line .* assertion x < 20: SUCCESS
+--

regression/goto-analyzer/pruning-lt-nondet/test-intervals.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--variable-sensitivity --vsd-values intervals --verify
+^EXIT=0$
+^SIGNAL=0$
+\[main\.assertion\.1\] line .* assertion x < 20: SUCCESS
+--

regression/goto-analyzer/pruning-lt-nondet/test-value-sets.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--variable-sensitivity --vsd-values set-of-constants --verify
+^EXIT=0$
+^SIGNAL=0$
+\[main\.assertion\.1\] line .* assertion x < 20: SUCCESS
+--

regression/goto-analyzer/pruning-lt/test-constants.desc

@@ -3,6 +3,5 @@ main.c
 --variable-sensitivity --vsd-values constants --verify
 ^EXIT=0$
 ^SIGNAL=0$
-\[main\.assertion\.1\] line .* assertion x < 20: UNKNOWN
-
+\[main\.assertion\.1\] line .* assertion x < 20: SUCCESS
 --