diff --git a/backend/cn/lib/testGeneration/genOptimize.ml b/backend/cn/lib/testGeneration/genOptimize.ml index bbf852d2f..ae3f4877c 100644 --- a/backend/cn/lib/testGeneration/genOptimize.ml +++ b/backend/cn/lib/testGeneration/genOptimize.ml @@ -2535,7 +2535,7 @@ module ConstraintPropagation = struct (Not, IT (Binop (EQ, IT (Const (Bits (_, n)), _, _), IT (Sym x, x_bt, _)), _, _)) -> let@ bt_rep = IntRep.of_bt x_bt in - Some (true, (x, Int (IntRep.intersect bt_rep (IntRep.ne n)))) + Some (false, (x, Int (IntRep.intersect bt_rep (IntRep.ne n)))) | Binop ( EQ, IT (Binop (Mod, IT (Sym x, x_bt, _), IT (Const (Bits (_, n)), _, _)), _, _), diff --git a/tests/cn-test-gen/src/neq.pass.c b/tests/cn-test-gen/src/neq.pass.c new file mode 100644 index 000000000..3eb993f74 --- /dev/null +++ b/tests/cn-test-gen/src/neq.pass.c @@ -0,0 +1,10 @@ +int ret_17_except_good(int x) +/*@ requires x != 10i32; + ensures return == 17i32; @*/ +{ + if (x == 10) { + return 23; + } else { + return 17; + } +}