diff --git a/src/include/yices.h b/src/include/yices.h index 2ed8a1735..6ed2c2a4e 100644 --- a/src/include/yices.h +++ b/src/include/yices.h @@ -2655,7 +2655,7 @@ __YICES_DLLSPEC__ extern void yices_garbage_collect(const term_t t[], uint32_t n * * The "mcsat" solver is required for formulas that use non-linear * arithmetic. If you select "mcsat" as the solver type, no other - * configuration is necessary. + * configuration is necessary (incremental and push-pop usages are enabled). * * If you select "dpllt" as the solver type, then you can define the * combination of theory solvers you want to include.