Add CaDiCaL make instructions

This commit adds the first instructions for building cbmc with
CaDiCaL 1.4.0 using the IPASIR interface in cbmc.

Author: TGWDB

COMPILING.md

@@ -380,6 +380,47 @@ For the packaged builds of CBMC on our release page we currently build CBMC
 with the MiniSat2 SAT solver statically linked at compile time. However it is
 also possible to build CBMC using alternative SAT solvers.
 
+### Compiling with CaDiCaL
+
+The [CaDiCaL](https://github.com/arminbiere/cadical) solver supports the
+[IPASIR](https://github.com/biotomas/ipasir) C interface to incremental SAT
+solvers, which is also supported by CBMC. So the process for producing a CBMC
+with CaDiCaL build is to build CaDiCaL as a static library then compile CBMC
+with the IPASIR build options and link to the CaDiCaL static library.
+
+Note that at the time of writing this has been tested to work with the CaDiCaL
+1.4.0 on Ubuntu 18.04 & 20.04.
+
+1. Download CaDiCaL:
+   ```
+   git clone --branch rel-1.4.0 https://github.com/arminbiere/cadical.git
+   ```
+   This will clone the CaDiCaL repository into a `cadical` subdirectory and
+   checkout release 1.4.0, which has been checked for compatibility with CBMC at
+   the time these instructions were written.
+
+2. Build CaDiCaL:
+   ```
+   cd cadical
+   ./configure
+   make cadical
+   cd ..
+   ```
+   This will create a build directory called `build` inside the clone of the
+   CaDiCaL repository. The `cadical` make target is specified in this example in
+   order to avoid building targets which are not required by CBMC. The built
+   static library will be placed in `cadical/build/libcadical.a`.
+
+3. Build CBMC:
+   ```
+   make -C src LIBS="$PWD/cadical/build/libcadical.a" IPASIR=$PWD/cadical/src
+   ```
+   This links the CaDiCaL library as part of the build. Passing the IPASIR
+   parameter tells the build system to build for the IPASIR interface. The
+   argument for the IPASIR parameter gives the build system the location for
+   the IPASIR headers, which is needed for the cbmc includes of `ipasir.h`. The
+   compiled binary will be placed in `cbmc/src/cbmc/cbmc`.
+
 ### Compiling with Riss
 
 The [Riss](https://github.com/conp-solutions/riss) solver supports the