Fix and enable COMPACT_LT_LE, needs re-eval

Author: tautschnig

src/solvers/flattening/bv_utils.cpp

@@ -1287,7 +1287,7 @@ literalt bv_utilst::equal(const bvt &op0, const bvt &op1)
 
 // 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
+#define COMPACT_LT_OR_LE
 
 
 
@@ -1313,7 +1313,7 @@ literalt bv_utilst::lt_or_le(
     compareBelow = prop.new_variables(bv0.size());
     result = prop.new_variable();
 
-    if(rep==SIGNED)
+    if(rep==representationt::SIGNED)
     {
       INVARIANT(
         bv0.size() >= 2, "signed bitvectors should have at least two bits");
@@ -1414,7 +1414,7 @@ literalt bv_utilst::unsigned_less_than(
   const bvt &op1)
 {
 #ifdef COMPACT_LT_OR_LE
-  return lt_or_le(false, op0, op1, UNSIGNED);
+  return lt_or_le(false, op0, op1, representationt::UNSIGNED);
 #else
   // A <= B  iff  there is an overflow on A-B
   return !carry_out(op0, inverted(op1), const_literal(true));