Function abstract_model 

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

Create an abstract model from initial state and predicates (legacy 2-arg API).

Without the transition relation, the abstract transition cannot be computed properly, so it defaults to the conjunction of predicates as a conservative overapproximation.