[CN-Test-Gen] Fix simplifying of != (#835)

rems-project · Jan 23, 2025 · e9a9261 · e9a9261
1 parent 3567800
commit e9a9261
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 1 deletion.
diff --git 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
@@ -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;
+  }
+}