updated abstraction.ml to use Z3.Expr module
renamed Prover.is_true to Prover.is_emp