sig
  val qe_lite :
    Z3.context -> Z3.AST.ASTVector.ast_vector -> Z3.Expr.expr -> Z3.Expr.expr
  val model_project :
    Z3.Model.model -> Z3.Expr.expr list -> Z3.Expr.expr -> Z3.Expr.expr
  val model_project_skolem :
    Z3.Model.model ->
    Z3.Expr.expr list ->
    Z3.Expr.expr -> Z3.AST.ASTMap.ast_map -> Z3.Expr.expr
  val model_project_with_witness :
    Z3.Model.model ->
    Z3.Expr.expr list ->
    Z3.Expr.expr -> Z3.AST.ASTMap.ast_map -> Z3.Expr.expr
end