Skip to content

Commit

Permalink
rm push/pop comment about mcsat
Browse files Browse the repository at this point in the history
  • Loading branch information
ahmed-irfan committed Jul 13, 2023
1 parent 9b2129c commit 3608896
Showing 1 changed file with 1 addition and 2 deletions.
3 changes: 1 addition & 2 deletions src/include/yices.h
Original file line number Diff line number Diff line change
Expand Up @@ -2654,8 +2654,7 @@ __YICES_DLLSPEC__ extern void yices_garbage_collect(const term_t t[], uint32_t n
* - mcsat: solver based on the Model-Constructing Satisfiability Calculus
*
* The "mcsat" solver is required for formulas that use non-linear
* arithmetic. Currently the mcsat solver does not support push and
* pop. If you select "mcsat" as the solver type, no other
* arithmetic. If you select "mcsat" as the solver type, no other
* configuration is necessary.
*
* If you select "dpllt" as the solver type, then you can define the
Expand Down

0 comments on commit 3608896

Please sign in to comment.