Function find_model 

pub fn find_model(e: &ProofExpr) -> ModelOutcome

Is e satisfiable? Returns a witnessing model over its atoms if so.

∃assignment. e. Tseitin-clausifies e, runs CDCL, and on SAT decodes the model back to the source atoms appearing in e (Tseitin auxiliaries are dropped). Used directly by bounded model checking (∃trace. ¬property) and for counterexample extraction.