Fix recognition of quantifier bounds in case of previous simplification of singleton interval

Author: NlightNFotis

regression/cbmc-primitives/alternating_quantifiers_6231/forall_in_exists.c

@@ -8,7 +8,7 @@ int main(int argc, char **argv)
 
     __CPROVER_assert(
         __CPROVER_exists { int z; (0 < z && z < 2) &&
-            __CPROVER_forall { int o; (10 < o && o < 20) ==> o > z && z == * i }},
+            __CPROVER_forall { int o; (10 < o && o < 20) ==> o > z && z == *i }},
         "there exists a z between 0 and 2 so that for all o between 10 and 20, o > z and z = 1");
 }
 // clang-format on

src/solvers/flattening/boolbv_quantifier.cpp

@@ -50,13 +50,13 @@ get_quantifier_var_min(const exprt &var_expr, const exprt &quantifier_expr)
   }
   else if(quantifier_expr.id() == ID_and)
   {
-    /**
-     * The min variable
-     * is in the form of "var_expr >= constant".
-     */
+    // The minimum variable can be of the form `var_expr >= constant`, or
+    // it can be of the form `var_expr == constant` (e.g. in the case where
+    // the interval that bounds the variable is a singleton interval (set
+    // with only one element)).
     for(auto &x : quantifier_expr.operands())
     {
-      if(x.id()!=ID_ge)
+      if(x.id() != ID_ge && x.id() != ID_equal)
         continue;
       const auto &x_binary = to_binary_relation_expr(x);
       if(expr_eq(var_expr, x_binary.lhs()) && x_binary.rhs().is_constant())
@@ -106,24 +106,42 @@ get_quantifier_var_max(const exprt &var_expr, const exprt &quantifier_expr)
   }
   else
   {
-    /**
-     * The max variable
-     * is in the form of "!(var_expr >= constant)".
-     */
+    // There are two potential forms we could come across here. The first one
+    // is `!(var_expr >= constant)` - identified by the first if branch - and
+    // the second is `var_expr == constant` - identified by the second else-if
+    // branch. The second form could be met if previous simplification has
+    // identified a singleton interval - see simplify_boolean_expr.cpp.
     for(auto &x : quantifier_expr.operands())
     {
-      if(x.id()!=ID_not)
-        continue;
-      exprt y = to_not_expr(x).op();
-      if(y.id()!=ID_ge)
-        continue;
-      const auto &y_binary = to_binary_relation_expr(y);
-      if(expr_eq(var_expr, y_binary.lhs()) && y_binary.rhs().is_constant())
+      if(x.id() == ID_not)
       {
-        const constant_exprt &over_expr = to_constant_expr(y_binary.rhs());
-        mp_integer over_i = numeric_cast_v<mp_integer>(over_expr);
-        over_i-=1;
-        return from_integer(over_i, y_binary.rhs().type());
+        exprt y = to_not_expr(x).op();
+        if(y.id() != ID_ge)
+          continue;
+        const auto &y_binary = to_binary_relation_expr(y);
+        if(expr_eq(var_expr, y_binary.lhs()) && y_binary.rhs().is_constant())
+        {
+          const constant_exprt &over_expr = to_constant_expr(y_binary.rhs());
+          mp_integer over_i = numeric_cast_v<mp_integer>(over_expr);
+          over_i -= 1;
+          return from_integer(over_i, y_binary.rhs().type());
+        }
+      }
+      else if(x.id() == ID_equal)
+      {
+        const auto &y_binary = to_binary_relation_expr(x);
+        if(expr_eq(var_expr, y_binary.lhs()) && y_binary.rhs().is_constant())
+        {
+          return to_constant_expr(y_binary.rhs());
+        }
+      }
+      else
+      {
+        // If we are here, we came across a (simplified?) expression that was
+        // not anticipated - normally this would be a bug, but if you made
+        // changes to the simplifier (as an example), you would need to add an
+        // else-if branch that handles that type above.
+        continue;
       }
     }
   }