Eager quantifier elimination: support empty ranges

conjunction(...) and disjunction(...) helper functions produce the
appropriate result for empty operand sequences.

Author: tautschnig

regression/cbmc/Quantifiers-invalid-var-range/test.desc

@@ -1,13 +1,11 @@
-KNOWNBUG broken-smt-backend
+CORE no-new-smt
 main.c
 
 ^\*\* Results:$
-^\*\* 0 of 1 failed
+^\*\* 0 of \d+ failed
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-This produces the expected verification result, but actually ignores some
-quantifiers.

src/solvers/flattening/boolbv_quantifier.cpp

@@ -217,9 +217,6 @@ static std::optional<exprt> eager_quantifier_instantiation(
   mp_integer lb = numeric_cast_v<mp_integer>(min_i.value());
   mp_integer ub = numeric_cast_v<mp_integer>(max_i.value());
 
-  if(lb > ub)
-    return {};
-
   auto expr_simplified =
     quantifier_exprt(expr.id(), expr.variables(), where_simplified);