Use CaDiCaL for selected THOROUGH regression tests

.github/workflows/pull-request-checks.yaml

@@ -411,7 +411,7 @@ jobs:
           git checkout -- memory_allocation1 printf1 union12 va_list3
           ../test.pl -c "cbmc --cprover-smt2" -I broken-smt-backend -K
 
-  # This job takes approximately 73 to 95 minutes
+  # This job takes approximately 8 to 30 minutes
   check-ubuntu-20_04-cmake-gcc-THOROUGH:
     runs-on: ubuntu-20.04
     steps:

jbmc/regression/jbmc-strings/VerifStringLastIndexOf/test.desc

@@ -1,6 +1,10 @@
 THOROUGH
 Test
---function Test.check --max-nondet-string-length 50 --unwind 50 --java-assume-inputs-non-null  --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
+--function Test.check --max-nondet-string-length 50 --unwind 50 --java-assume-inputs-non-null  --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --sat-solver cadical
 VERIFICATION SUCCESSFUL
 ^EXIT=0$
 ^SIGNAL=0$
+--
+--
+This test takes approximately 3 minutes when using MiniSat, and less than 1
+minute when using CaDiCaL.

jbmc/regression/jbmc-strings/java_easychair/test.desc

@@ -1,7 +1,10 @@
 THOROUGH
 easychair
---max-nondet-string-length 1000
+--max-nondet-string-length 1000 --sat-solver cadical
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\].* line 30.* FAILURE$
 --
+--
+This test takes approximately 2 minutes when using MiniSat, and just 20 seconds
+when using CaDiCaL.

jbmc/regression/strings-smoke-tests/java_parselong_unknown_radix/test.desc

@@ -1,9 +1,12 @@
 THOROUGH
 Test
---max-nondet-string-length 10 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --function Test.testMe --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
+--max-nondet-string-length 10 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --function Test.testMe --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --sat-solver cadical
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 12.* FAILURE$
 ^\[.*assertion.2\].* line 14.* SUCCESS$
 --
 non equal types
+--
+This test takes approximately 45 minutes when using MiniSat, but less than 1
+minute when using CaDiCaL.

regression/cbmc/Float-equality1/test_equality.desc

@@ -1,12 +1,12 @@
 THOROUGH
 main.c
--DEQUALITY
+-DEQUALITY --sat-solver cadical
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
 --
 Takes approximately 1000 seconds to complete when using the SAT back-end (and
-Minisat2). The SMT solver completes this task in less than 0.1 seconds.
-See #4337.
+Minisat2). CaDiCaL solves the problem in less than 2 minutes. The SMT solver
+completes this task in less than 0.1 seconds.  See #4337.

regression/cbmc/gcc_popcount2/test.desc

@@ -1,10 +1,13 @@
 THOROUGH
 main.c
-
+--sat-solver cadical
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
 \[main\.assertion\.\d+\] line 39 assertion sizeof\(ull\) != sizeof\(unsigned int\) && pop4\(ull\) == __builtin_popcount\(ull\): FAILURE$
 ^\*\* 1 of 3 failed
 --
 ^warning: ignoring
+--
+MiniSat takes approximately 1 hour on this test while CaDiCaL completes in under
+3 minutes.