Skip to content

Commit bb63a73

Browse files
author
Enrico Steffinlongo
committed
Added man entry for --incremental-smt2-solver
1 parent 52dfb5c commit bb63a73

File tree

1 file changed

+5
-0
lines changed

1 file changed

+5
-0
lines changed

doc/man/cbmc.1

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -176,6 +176,11 @@ Output formula to given file
176176
Never turn arrays into uninterpreted functions
177177
.IP --arrays-uf-always
178178
Always turn arrays into uninterpreted functions
179+
.IP "--incremental-smt2-solver <cmd>"
180+
Use the incremental SMT backend where <cmd> is the command to invoke the SMT
181+
solver of choice using incremental mode and accepting input from the standard input.
182+
Note that the solver name must be in the "PATH" or be an executable with full
183+
path. Also the flag --slice-formula should be added to remove some not-yet supoorted features.
179184
.SH ENVIRONMENT
180185
All tools honor the TMPDIR environment variable when generating temporary
181186
files and directories. Furthermore note that

0 commit comments

Comments
 (0)