Skip to content

Commit 3aaafd9

Browse files
committed
Clarify the logic that the build system uses for setting the default solver
1 parent 02d10d2 commit 3aaafd9

File tree

1 file changed

+6
-2
lines changed

1 file changed

+6
-2
lines changed

COMPILING.md

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -392,8 +392,12 @@ For example, to build CBMC with MiniSAT2 and Glucose, do:
392392
make -C src minisat2-download glucose-download
393393
make -C src MINISAT2=../../minisat-2.2.1 GLUCOSE=../../glucose-syrup
394394
```
395-
In that case, MiniSAT2 will be used by default. To switch to glucose at runtime,
396-
run CBMC with `--sat-solver glucose`.
395+
The build sets the default solver based on the priority defined by the
396+
`#if/#elif` tree defined at the end of
397+
[`src/solvers/sat/satcheck.h`](https://github.com/diffblue/cbmc/blob/develop/src/solvers/sat/satcheck.h).
398+
In the above example, MiniSAT2 will be set as the default solver because it is
399+
listed before Glucose. To switch to glucose at runtime, run CBMC with
400+
`--sat-solver glucose`.
397401
398402
For CMake the alternatives can be built with the following arguments to `cmake`
399403
for glucose `-Dsat_impl=glucose`.

0 commit comments

Comments
 (0)