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 #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.

INCLUDE_REDUNDANT_CLAUSES is not enabled: while this would yield a further
speed-up of 1080.4 seconds with CaDiCaL, it slows down Minisat by 4440.6
seconds on the above benchmark set.

Author: tautschnig

jbmc/regression/jbmc/assume-inputs-non-null/string_assume.desc

@@ -1,4 +1,4 @@
-CORE
+THOROUGH
 My
 --function My.stringArg --java-assume-inputs-non-null
 ^EXIT=10$
@@ -10,3 +10,6 @@ My
 ^warning: ignoring
 --
 Check that --java-assume-inputs-non-null restricts inputs to non-null strings
+
+The test is marked "THOROUGH" as it requires more memory than may be available
+on some GitHub runners.

jbmc/regression/jbmc/exceptions29/test.desc

@@ -1,4 +1,4 @@
-CORE
+THOROUGH
 test
 --unwind 10
 ^\[java::test.main:\(\[Ljava/lang/String;\)V\.assertion.1\] line 14 assertion at file test\.java line 14 function java::test.main:\(\[Ljava/lang/String;\)V bytecode-index 21: FAILURE$
@@ -15,3 +15,6 @@ test.main gives the following exception table:
     8    22    25   Class java/lang/Exception
     0     7    45   Class MyException
     8    42    45   Class MyException
+
+The test is marked "THOROUGH" as it requires more memory than may be available
+on some GitHub runners.

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,