allow empty bit-vector if

Author: Daniel Kroening

regression/cbmc/Empty_struct1/main.c

@@ -0,0 +1,16 @@
+#include <assert.h>
+
+struct empty
+{
+};
+
+int main()
+{
+  struct empty e1, e2, e3;
+  _Bool b, c=b;
+  e1=e2;
+  if(b)
+    e3=e2;
+
+  assert(b==c);
+}

regression/cbmc/Empty_struct1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/solvers/flattening/boolbv_if.cpp

@@ -25,7 +25,7 @@ bvt boolbvt::convert_if(const if_exprt &expr)
   std::size_t width=boolbv_width(expr.type());
 
   if(width==0)
-    return conversion_failed(expr);
+    return bvt(); // An empty bit-vector if.
 
   literalt cond=convert(expr.cond());