diff --git a/regression/cbmc/constant_folding3/main.c b/regression/cbmc/constant_folding3/main.c new file mode 100644 index 00000000000..4d53aa377b4 --- /dev/null +++ b/regression/cbmc/constant_folding3/main.c @@ -0,0 +1,8 @@ +int main(void) +{ + int x; + int plus_one_is_null = &x + 1 == (int *)0 ? 1 : 0; + __CPROVER_assert(plus_one_is_null != 2, "cannot be 2"); + + return 0; +} diff --git a/regression/cbmc/constant_folding3/test.desc b/regression/cbmc/constant_folding3/test.desc new file mode 100644 index 00000000000..30d812ee484 --- /dev/null +++ b/regression/cbmc/constant_folding3/test.desc @@ -0,0 +1,9 @@ +CORE new-smt-backend +main.c + +^Generated 1 VCC\(s\), 0 remaining after simplification$ +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/src/util/expr_util.cpp b/src/util/expr_util.cpp index 96ac38827dd..089dc217aa2 100644 --- a/src/util/expr_util.cpp +++ b/src/util/expr_util.cpp @@ -239,8 +239,12 @@ bool is_constantt::is_constant(const exprt &expr) const expr.id() == ID_typecast || expr.id() == ID_array_of || expr.id() == ID_plus || expr.id() == ID_mult || expr.id() == ID_array || expr.id() == ID_with || expr.id() == ID_struct || expr.id() == ID_union || - expr.id() == ID_empty_union || - expr.id() == ID_byte_update_big_endian || + expr.id() == ID_empty_union || expr.id() == ID_equal || + expr.id() == ID_notequal || expr.id() == ID_lt || expr.id() == ID_le || + expr.id() == ID_gt || expr.id() == ID_ge || expr.id() == ID_if || + expr.id() == ID_not || expr.id() == ID_and || expr.id() == ID_or || + expr.id() == ID_bitnot || expr.id() == ID_bitand || expr.id() == ID_bitor || + expr.id() == ID_bitxor || expr.id() == ID_byte_update_big_endian || expr.id() == ID_byte_update_little_endian) { return std::all_of(