[smt_convt] Fix comparison of invalid pointers

The SMT conversion routines crashed on encoding of comparisons over invalid
pointers.
This change fixes this behavior by ignoring comparisons against invalid
pointers.

Author: SaswatPadhi

regression/cbmc/memset_null/main.c

@@ -0,0 +1,9 @@
+#include <stdlib.h>
+#include <string.h>
+
+void main()
+{
+  char *data = nondet() ? NULL : malloc(8);
+  memset(data, 0, 8);
+  memset(data, 0, 8);
+}

regression/cbmc/memset_null/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+
+^\[main.precondition_instance.1\] line .* memset destination region writeable: FAILURE$
+^\[main.precondition_instance.2\] line .* memset destination region writeable: FAILURE$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+This test case checks that byte operations (e.g. memset) oninvalid and `NULL`
+pointers are correctly encoded in SMT2.

src/solvers/smt2/smt2_conv.cpp

@@ -4247,6 +4247,11 @@ void smt2_convt::set_to(const exprt &expr, bool value)
   if(expr.id() == ID_equal && value)
   {
     const equal_exprt &equal_expr=to_equal_expr(expr);
+    if(equal_expr.lhs().type().id() == ID_empty)
+    {
+      // ignore equality checking on pointers with empty type
+      return;
+    }
 
     if(equal_expr.lhs().id()==ID_symbol)
     {