pub fn interpolate(a: &VerifyExpr, b: &VerifyExpr) -> Option<VerifyExpr>Expand description
Compute a Craig interpolant approximation.
Given formulas A and B where A AND B is UNSAT, returns an over-approximation of A that uses only variables shared between A and B, and is still inconsistent with B.
Returns None if A AND B is SAT (no interpolant exists).