Enable compact less-than propositional encoding

This was previously disabled as it appeared to degrade performance. New
benchmarking, however, suggests considerable performance improvement:

When running on various proofs done for AWS open-source projects, this
changes the performance as follows (when comparing to diffblue#7021): with
CaDiCaL as back-end, the total solver time for the hardest 46 proofs
changes from 26779.7 to 24472.6 seconds (2307.1 seconds speed-up); with
Minisat the hardest 49 proofs take 18541.2 instead of 28420.4
seconds (9879.2 seconds speed-up). Across these benchmarks, 1.0% of
variables and 3.2% of clauses are removed.

Author: tautschnig

src/solvers/flattening/bv_utils.cpp

@@ -1198,17 +1198,13 @@ literalt bv_utilst::equal(const bvt &op0, const bvt &op1)
 /// \par parameters: bvts for each input and whether they are signed and whether
 /// a model of < or <= is required.
 /// \return A literalt that models the value of the comparison.
+
+#define COMPACT_LT_OR_LE
 /* Some clauses are not needed for correctness but they remove
    models (effectively setting "don't care" bits) and so may be worth
    including.*/
 // #define INCLUDE_REDUNDANT_CLAUSES
 
-// Saves space but slows the solver
-// There is a variant that uses the xor as an auxiliary that should improve both
-// #define COMPACT_LT_OR_LE
-
-
-
 literalt bv_utilst::lt_or_le(
   bool or_equal,
   const bvt &bv0,