Update installation instructions to include how to build CBMC with multiple backend solvers

Author: zhassan-aws

COMPILING.md

@@ -82,7 +82,7 @@ files.
    to generate IDE projects by supplying the `-G` flag.  Run `cmake -G` for a
    comprehensive list of supported back-ends.
 
-   As part of this step, CMake will download the back-end solver (see Section
+   As part of this step, CMake will download the back-end solvers (see Section
    "Compiling with alternative SAT solvers" in this document for configuration
    options). Should it be necessary to perform this step without network access,
    a solver can be downloaded ahead of the above `cmake` invocation as follows:
@@ -371,28 +371,40 @@ compilation flag:
 ## Compiling with alternative SAT solvers
 
 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.
+with the MiniSat2 and CaDiCaL SAT solvers statically linked at compile time.
+However it is also possible to build CBMC using alternative SAT solvers.
 
 ### Compiling CBMC Using Solver Native Interfaces
 
 The following solvers are supported by CBMC using custom interfaces and can
-by downloaded and compiled by the build process: MiniSAT2, CaDiCaL, and Glucose.
+be downloaded and compiled by the build process: MiniSAT2, CaDiCaL, and Glucose.
 
-For `make` alternatives to the default (i.e. not MiniSAT) can be built with the
-following commands for CaDiCaL:
-```
-make -C src cadical-download
-make -C src CADICAL=../../cadical
-```
-and for glucose
+For `make`, alternatives to the default (i.e. not MiniSAT and CaDiCaL) can be
+built with the following commands for glucose:
 ```
 make -C src glucose-download
 make -C src GLUCOSE=../../glucose-syrup
 ```
+CBMC can be built with multiple solvers, which can then be selected at runtime
+using the `--sat-solver` option.
+For example, to build CBMC with MiniSAT2 and Glucose, do:
+```
+make -C src minisat2-download glucose-download
+make -C src MINISAT2=../../minisat-2.2.1 GLUCOSE=../../glucose-syrup
+```
+The build sets the default solver based on the priority defined by the
+`#if/#elif` tree defined at the end of
+[`src/solvers/sat/satcheck.h`](https://github.com/diffblue/cbmc/blob/develop/src/solvers/sat/satcheck.h).
+In the above example, MiniSAT2 will be set as the default solver because it is
+listed before Glucose. To switch to glucose at runtime, run CBMC with
+`--sat-solver glucose`.
 
 For CMake the alternatives can be built with the following arguments to `cmake`
-for CaDiCaL `-Dsat_impl=cadical` and for glucose `-Dsat_impl=glucose`.
+for glucose `-Dsat_impl=glucose`.
+To build CBMC with multiple solvers, specify the solvers in a semicolon-separated list to `-Dsat_impl`, e.g.:
+```
+cmake -S . -Bbuild -Dsat_impl="minisat2;glucose"
+```
 
 
 ### Compiling with IPASIR Interface
@@ -520,7 +532,7 @@ successfully on Windows or macOS.
 This document assumes you have already been able to build CPROVER on
 your chosen architecture.
 
-#RUNNING REGRESSION AND UNIT TESTS
+# RUNNING REGRESSION AND UNIT TESTS
 
 Regression and unit tests can be run using cmake or make. Your choice here
 should be the same as the compiling of the project itself.