Omit binary value from xml if it is absent in the trace

There are instances when running with `--cprover-smt2` where the type of
the expression is `bitvector_typet`, but the expression is not a
`constant_exprt`. By removing the printing in this case we can avoid
breaking the partial functionality available with the `--cprover-smt2`
option.

Author: thomasspriggs

src/goto-programs/xml_goto_trace.cpp

@@ -34,14 +34,15 @@ xmlt full_lhs_value(const goto_trace_stept &step, const namespacet &ns)
     lhs_object.has_value() ? lhs_object->get_identifier() : irep_idt();
 
   const exprt &value = step.full_lhs_value;
-  if(value.is_not_nil())
-    xml.data = from_expr(ns, identifier, value);
+  if(value.is_nil())
+    return xml;
 
-  if(const auto &type = type_try_dynamic_cast<bitvector_typet>(value.type()))
+  xml.data = from_expr(ns, identifier, value);
+  const auto &bv_type = type_try_dynamic_cast<bitvector_typet>(value.type());
+  const auto &constant = expr_try_dynamic_cast<constant_exprt>(value);
+  if(bv_type && constant)
   {
-    const auto &constant =
-      expr_try_dynamic_cast<constant_exprt>(value);
-    const auto width = type->get_width();
+    const auto width = bv_type->get_width();
     const auto binary_representation =
       integer2binary(bvrep2integer(constant->get_value(), width, false), width);
     xml.set_attribute("binary", binary_representation);