From a86c4d9562825fad6badd07d774884c5455db3ec Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Mon, 15 Oct 2018 12:45:13 +0000
Subject: [PATCH] Distinguish __CPROVER_bool from _Bool in output

A __CPROVER_bool is a single bit and should not be output the same way as a
_Bool, which may be one or more bytes wide.
---
 regression/cbmc/cprover_bool1/main.c    |  8 ++++++++
 regression/cbmc/cprover_bool1/test.desc | 10 ++++++++++
 src/ansi-c/expr2c.cpp                   |  2 +-
 3 files changed, 19 insertions(+), 1 deletion(-)
 create mode 100644 regression/cbmc/cprover_bool1/main.c
 create mode 100644 regression/cbmc/cprover_bool1/test.desc

diff --git a/regression/cbmc/cprover_bool1/main.c b/regression/cbmc/cprover_bool1/main.c
new file mode 100644
index 00000000000..f9af057ad0c
--- /dev/null
+++ b/regression/cbmc/cprover_bool1/main.c
@@ -0,0 +1,8 @@
+#include <assert.h>
+
+int main()
+{
+  int y;
+  __CPROVER_bool x = y;
+  assert(x != (__CPROVER_bool)y);
+}
diff --git a/regression/cbmc/cprover_bool1/test.desc b/regression/cbmc/cprover_bool1/test.desc
new file mode 100644
index 00000000000..20a1bea26ec
--- /dev/null
+++ b/regression/cbmc/cprover_bool1/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--trace
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+x != \(__CPROVER_bool\)y
+--
+x != \(_Bool\)y
+^warning: ignoring
diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
index 5e8572e82b1..05e779af40a 100644
--- a/src/ansi-c/expr2c.cpp
+++ b/src/ansi-c/expr2c.cpp
@@ -205,7 +205,7 @@ std::string expr2ct::convert_rec(
 
   if(src.id()==ID_bool)
   {
-    return q+"_Bool"+d;
+    return q + CPROVER_PREFIX + "bool" + d;
   }
   else if(src.id()==ID_c_bool)
   {