From 439bb2c0ccee3dc0e7fb89a6ecceb9e413cbff6b Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Thu, 12 Oct 2023 08:53:03 +0000
Subject: [PATCH] Simplification towards singleton intervals requires single
 variable

We must not blindly assume that that <exprA> and <exprB> in
<exprA> >= C1 && !(<exprB> >= C2) are the same.

Fixes: #7953
---
 .../cbmc/simplify_singleton_interval_7953/main.c      | 11 +++++++++++
 .../cbmc/simplify_singleton_interval_7953/test.desc   | 10 ++++++++++
 src/util/simplify_expr_boolean.cpp                    |  4 ++++
 3 files changed, 25 insertions(+)
 create mode 100644 regression/cbmc/simplify_singleton_interval_7953/main.c
 create mode 100644 regression/cbmc/simplify_singleton_interval_7953/test.desc

diff --git a/regression/cbmc/simplify_singleton_interval_7953/main.c b/regression/cbmc/simplify_singleton_interval_7953/main.c
new file mode 100644
index 00000000000..9595ce5e313
--- /dev/null
+++ b/regression/cbmc/simplify_singleton_interval_7953/main.c
@@ -0,0 +1,11 @@
+#include <assert.h>
+extern void __VERIFIER_assume(int cond);
+extern int __VERIFIER_nondet_int(void);
+int main()
+{
+  int z = __VERIFIER_nondet_int();
+  int k = __VERIFIER_nondet_int();
+  __VERIFIER_assume(1 < z);
+  __VERIFIER_assume(1 <= z && k <= 1);
+  assert(0);
+}
diff --git a/regression/cbmc/simplify_singleton_interval_7953/test.desc b/regression/cbmc/simplify_singleton_interval_7953/test.desc
new file mode 100644
index 00000000000..e1db0def910
--- /dev/null
+++ b/regression/cbmc/simplify_singleton_interval_7953/test.desc
@@ -0,0 +1,10 @@
+CORE new-smt-backend
+main.c
+
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Simplification must not spuriously turn the second assumption into an equality.
diff --git a/src/util/simplify_expr_boolean.cpp b/src/util/simplify_expr_boolean.cpp
index 247979f8426..585b2254f8d 100644
--- a/src/util/simplify_expr_boolean.cpp
+++ b/src/util/simplify_expr_boolean.cpp
@@ -151,6 +151,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_boolean(const exprt &expr)
       {
         mp_integer lower;
         mp_integer higher;
+        exprt non_const_value;
       };
       boundst bounds;
 
@@ -177,6 +178,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_boolean(const exprt &expr)
             auto int_opt =
               numeric_cast<mp_integer>(to_constant_expr(ge_expr->rhs())))
           {
+            bounds.non_const_value = ge_expr->lhs();
             bounds.lower = *int_opt;
             return true;
           }
@@ -199,6 +201,8 @@ simplify_exprt::resultt<> simplify_exprt::simplify_boolean(const exprt &expr)
             // (e.g. i >= j)
             if(!ge_expr->rhs().is_constant())
               return false;
+            if(ge_expr->lhs() != bounds.non_const_value)
+              return false;
             if(
               auto int_opt =
                 numeric_cast<mp_integer>(to_constant_expr(ge_expr->rhs())))