Merge pull request #3182 from tautschnig/cprover_bool-output

Distinguish __CPROVER_bool from _Bool in output

Author: Daniel Kroening

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);
+}

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

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)
   {