kdrag.theories.real.abstract_arith

kdrag.theories.real.abstract_arith(t: ExprRef) → ExprRef

Z3 has difficult ematching over arithmetic expressions. Abstracting them to uninterpreted functions can help.