Merge pull request #7954 from tautschnig/bugfixes/7953-interval-simp

Simplification towards singleton intervals requires single variable

Author: TGWDB

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

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.

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())))