Skip to content

Commit a22fb03

Browse files
committed
Improve documentation clarity
Improves clarity of the documentation for building CBMC with alternative SAT solvers.
1 parent a89fc93 commit a22fb03

File tree

1 file changed

+7
-3
lines changed

1 file changed

+7
-3
lines changed

COMPILING.md

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -380,7 +380,7 @@ For the packaged builds of CBMC on our release page we currently build CBMC
380380
with the MiniSat2 SAT solver statically linked at compile time. However it is
381381
also possible to build CBMC using alternative SAT solvers.
382382
383-
### Compiling with CBMC Wrapper
383+
### Compiling CBMC Using Solver Native Interfaces
384384
385385
The following solvers are supported by CBMC using custom interfaces and can
386386
by downloaded and compiled by the build process: MiniSAT2, CaDiCaL, and Glucose.
@@ -417,7 +417,11 @@ Where `SATOBJ` is the pre-compiled IPASIR compatible SAT binary,
417417
The rest of this section provides detailed instructions for some example
418418
SAT solvers.
419419
420-
#### Compiling with CaDiCaL
420+
#### Compiling with CaDiCaL via IPASIR
421+
422+
Note that CaDiCaL can also be built using CBMC's CaDiCaL native interface
423+
as described above. This section is to use CaDiCaL with the IPASIR
424+
interface in CBMC.
421425
422426
The [CaDiCaL](https://github.com/arminbiere/cadical) solver supports the
423427
[IPASIR](https://github.com/biotomas/ipasir) C interface to incremental SAT
@@ -458,7 +462,7 @@ Note that at the time of writing this has been tested to work with the CaDiCaL
458462
the IPASIR headers, which is needed for the cbmc includes of `ipasir.h`. The
459463
compiled binary will be placed in `cbmc/src/cbmc/cbmc`.
460464
461-
#### Compiling with Riss
465+
#### Compiling with Riss via IPASIR
462466
463467
The [Riss](https://github.com/conp-solutions/riss) solver supports the
464468
[IPASIR](https://github.com/biotomas/ipasir) C interface to incremental SAT

0 commit comments

Comments
 (0)