Function prove_valid 

pub fn prove_valid(pred: &VerifyExpr) -> EquivalenceResult

Prove that a Bool-sorted VerifyExpr is valid (true under every assignment of its free variables).

Implemented as an equivalence check against the constant true: the backend asserts ¬(pred ↔ true) and asks Z3 for a model. Unsat ⇒ the predicate is valid ([EquivalenceResult::Equivalent]); Sat ⇒ a counterexample assignment ([EquivalenceResult::NotEquivalent]).