Function abstract_model_full 

pub fn abstract_model_full(
    init: &VerifyExpr,
    transition: &VerifyExpr,
    predicates: &[VerifyExpr],
) -> AbstractModel

Create an abstract model with Cartesian predicate abstraction.

Given concrete init, transition, and a set of predicates, this computes:

• abstract_init: init AND conjunction of all predicates
• abstract_transition: concrete transition AND inductive predicate implications

For each predicate p_i, we check via Z3 whether p_i is inductive relative to the transition: (p_i@t AND T(t, t1)) => p_i@t1. If valid (UNSAT negation), the implication is included in the abstract transition. If not valid, the predicate may take any value in the next state (overapproximation).

This is Cartesian predicate abstraction: each predicate is checked independently.