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