Merge pull request #7068 from tautschnig/feature/enable-compact-le-or-lt

Enable compact less-than propositional encoding

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,