diff --git a/regression/cbmc/Empty_struct1/main.c b/regression/cbmc/Empty_struct1/main.c new file mode 100644 index 0000000000..b1d7a0b781 --- /dev/null +++ b/regression/cbmc/Empty_struct1/main.c @@ -0,0 +1,16 @@ +#include + +struct empty +{ +}; + +int main() +{ + struct empty e1, e2, e3; + _Bool b, c=b; + e1=e2; + if(b) + e3=e2; + + assert(b==c); +} diff --git a/regression/cbmc/Empty_struct1/test.desc b/regression/cbmc/Empty_struct1/test.desc new file mode 100644 index 0000000000..9efefbc736 --- /dev/null +++ b/regression/cbmc/Empty_struct1/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/src/solvers/flattening/boolbv_if.cpp b/src/solvers/flattening/boolbv_if.cpp index 535f87bc01..30b3533f2d 100644 --- a/src/solvers/flattening/boolbv_if.cpp +++ b/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());