From e9a9261b55f44900780ec6aa0bd230f1e5ae7c02 Mon Sep 17 00:00:00 2001
From: Zain K Aamer <ZippeyKeys12@gmail.com>
Date: Thu, 23 Jan 2025 18:13:17 -0500
Subject: [PATCH] [CN-Test-Gen] Fix simplifying of `!=` (#835)

---
 backend/cn/lib/testGeneration/genOptimize.ml |  2 +-
 tests/cn-test-gen/src/neq.pass.c             | 10 ++++++++++
 2 files changed, 11 insertions(+), 1 deletion(-)
 create mode 100644 tests/cn-test-gen/src/neq.pass.c

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;
+  }
+}