From 69dc74923908206f0a568ee89fd6cc1c8392802c Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Sat, 17 Nov 2018 21:02:00 +0700 Subject: [PATCH] Fix missing word in doc comment. --- src/api/z3_api.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index e1359949d..be463b1b0 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -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.