Merge pull request #6517 from tautschnig/quantifiers-unsigned

Flattening: support quantifiers over unsigned variables

Author: tautschnig

regression/cbmc/Quantifiers-type/main.c

@@ -1,16 +1,13 @@
 int main()
 {
   int a[2];
-  int b[2];
 
   // clang-format off
   // clang-format would rewrite the "==>" as "== >"
   __CPROVER_assume( __CPROVER_forall { float i; (i>=0 && i<2) ==> a[i]>=10 && a[i]<=10 } );
-  __CPROVER_assume( __CPROVER_forall { char i; (i>=0 && i<2) ==> b[i]>=10 && b[i]<=10 } );
   // clang-format on
 
   assert(a[0]==10 && a[1]==10);
-  assert(b[0]==10 && b[1]==10);
 
   return 0;
 }

regression/cbmc/Quantifiers-type/test.desc

@@ -3,8 +3,7 @@ main.c
 
 ^\*\* Results:$
 ^\[main.assertion.1\] line 12 assertion tmp_if_expr(\$\d+)?: FAILURE$
-^\[main.assertion.2\] line 13 assertion tmp_if_expr\$\d+: SUCCESS$
-^\*\* 1 of 2 failed
+^\*\* 1 of 1 failed
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$

regression/cbmc/Quantifiers-type2/main.c

@@ -0,0 +1,16 @@
+int main()
+{
+  int b[2];
+  int c[2];
+
+  // clang-format off
+  // clang-format would rewrite the "==>" as "== >"
+  __CPROVER_assume( __CPROVER_forall { char i; (i>=0 && i<2) ==> b[i]>=10 && b[i]<=10 } );
+  __CPROVER_assume( __CPROVER_forall { unsigned i; (i>=0 && i<2) ==> c[i]>=10 && c[i]<=10 } );
+  // clang-format on
+
+  assert(b[0] == 10 && b[1] == 10);
+  assert(c[0] == 10 && c[1] == 10);
+
+  return 0;
+}

regression/cbmc/Quantifiers-type2/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+
+^\*\* Results:$
+^\[main.assertion.1\] line 12 assertion tmp_if_expr(\$\d+)?: SUCCESS$
+^\[main.assertion.2\] line 13 assertion tmp_if_expr\$\d+: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

src/solvers/flattening/boolbv_quantifier.cpp

@@ -48,6 +48,9 @@ get_quantifier_var_min(const exprt &var_expr, const exprt &quantifier_expr)
         return to_constant_expr(y_binary.rhs());
       }
     }
+
+    if(var_expr.type().id() == ID_unsignedbv)
+      return from_integer(0, var_expr.type());
   }
   else if(quantifier_expr.id() == ID_and)
   {
@@ -66,6 +69,9 @@ get_quantifier_var_min(const exprt &var_expr, const exprt &quantifier_expr)
         return to_constant_expr(x_binary.rhs());
       }
     }
+
+    if(var_expr.type().id() == ID_unsignedbv)
+      return from_integer(0, var_expr.type());
   }
 
   return {};