mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
Fix missing word in doc comment.
This commit is contained in:
parent
a000747605
commit
69dc749239
|
@ -5579,7 +5579,7 @@ extern "C" {
|
|||
\brief Convert a goal into a DIMACS formatted string.
|
||||
The goal must be in CNF. You can convert a goal to CNF
|
||||
by applying the tseitin-cnf tactic. Bit-vectors are not automatically
|
||||
converted to Booleans either, so the caller intends to
|
||||
converted to Booleans either, so if the caller intends to
|
||||
preserve satisfiability, it should apply bit-blasting tactics.
|
||||
Quantifiers and theory atoms will not be encoded.
|
||||
|
||||
|
|
Loading…
Reference in a new issue