diff --git a/regression/cbmc/c99_Bool/main.c b/regression/cbmc/c99_Bool/main.c
new file mode 100644
index 00000000000..532ff6e2efe
--- /dev/null
+++ b/regression/cbmc/c99_Bool/main.c
@@ -0,0 +1,11 @@
+#include <assert.h>
+
+void foo(_Bool y)
+{
+  int x;
+  if(y) 
+  {  
+    x=(int)y;
+    assert(x==1);
+  }
+}
diff --git a/regression/cbmc/c99_Bool/test.desc b/regression/cbmc/c99_Bool/test.desc
new file mode 100644
index 00000000000..a454c448ed0
--- /dev/null
+++ b/regression/cbmc/c99_Bool/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--function foo
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/src/ansi-c/ansi_c_entry_point.cpp b/src/ansi-c/ansi_c_entry_point.cpp
index 1acfb7d4459..1e7f8922262 100644
--- a/src/ansi-c/ansi_c_entry_point.cpp
+++ b/src/ansi-c/ansi_c_entry_point.cpp
@@ -74,6 +74,18 @@ exprt::operandst build_function_environment(
 
     init_code.add(decl);
 
+    // nondet init for _Bool
+    if(decl.symbol().type().id()==ID_c_bool)
+    {
+      code_assignt assign(
+        decl.symbol(),
+        typecast_exprt(
+          side_effect_expr_nondett(bool_typet()),
+          decl.symbol().type()));
+
+      init_code.move_to_operands(assign);
+    }
+
     codet input(ID_input);
     input.operands().resize(2);
 
diff --git a/src/util/json_expr.cpp b/src/util/json_expr.cpp
index 7fd4f265f3f..727449340dc 100644
--- a/src/util/json_expr.cpp
+++ b/src/util/json_expr.cpp
@@ -266,6 +266,15 @@ json_objectt json(
       result["binary"]=json_stringt(expr.is_true()?"1":"0");
       result["data"]=jsont::json_boolean(expr.is_true());
     }
+    else if(type.id()==ID_c_bool)
+    {
+      result["name"]=json_stringt("integer");
+      result["c_type"]=json_stringt("_Bool");
+      result["binary"]=json_stringt(expr.get_string(ID_value));
+      mp_integer b;
+      to_integer(to_constant_expr(expr), b);
+      result["data"]=json_stringt(integer2string(b));
+    }
     else
     {
       result["name"]=json_stringt("unknown");
diff --git a/src/util/xml_expr.cpp b/src/util/xml_expr.cpp
index 11a4ac1d2c6..6eb49b8261b 100644
--- a/src/util/xml_expr.cpp
+++ b/src/util/xml_expr.cpp
@@ -126,7 +126,8 @@ xmlt xml(
   {
     result.name="vector";
     result.new_element("subtype").new_element()=xml(type.subtype(), ns);
-    result.new_element("size").new_element()=xml(to_vector_type(type).size(), ns);
+    result.new_element("size").new_element()=
+      xml(to_vector_type(type).size(), ns);
   }
   else if(type.id()==ID_struct)
   {
@@ -263,6 +264,15 @@ xmlt xml(
       result.set_attribute("binary", expr.is_true()?"1":"0");
       result.data=expr.is_true()?"TRUE":"FALSE";
     }
+    else if(type.id()==ID_c_bool)
+    {
+      result.name="integer";
+      result.set_attribute("c_type", "_Bool");
+      result.set_attribute("binary", expr.get_string(ID_value));
+      mp_integer b;
+      to_integer(to_constant_expr(expr), b);
+      result.data=integer2string(b);
+    }
     else
     {
       result.name="unknown";
@@ -309,7 +319,8 @@ xmlt xml(
 
     xmlt &e=result.new_element("member");
     e.new_element(xml(expr.op0(), ns));
-    e.set_attribute("member_name",
+    e.set_attribute(
+      "member_name",
       id2string(to_union_expr(expr).get_component_name()));
   }
   else