Function block_model_values 

pub unsafe extern "C" fn block_model_values(
    cvc5: *mut Solver,
    size: usize,
    terms: *const Term,
)

Block the current model values of (at least) the values in terms. Can be called only if immediately preceded by a SAT query.

SMT-LIB:

\verbatim embed:rst:leading-asterisk .. code:: smtlib

(block-model-values ( <terms>+ ))

Requires enabling option :ref:produce-models <lbl-option-produce-models>. \endverbatim

@warning This function is experimental and may change in future versions. @param cvc5 The solver instance. @param size The number of values to block. @param terms The values to block.