Changes before error encountered

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

Author: Copilot

src/ast/ast_util.h

@@ -103,6 +103,7 @@ expr * mk_and(ast_manager & m, unsigned num_args, expr * const * args);
 app  * mk_and(ast_manager & m, unsigned num_args, app * const * args);
 inline expr * mk_and(ast_manager & m, ptr_vector<expr> const& args) { return mk_and(m, args.size(), args.data()); }
 inline expr * mk_and(ast_manager & m, ptr_buffer<expr> const& args) { return mk_and(m, args.size(), args.data()); }
+inline expr * mk_and(ast_manager & m, expr* a, expr* b) { expr* args[2] = { a, b }; return mk_and(m, 2, args); }
 inline expr * mk_and(ast_manager & m, std::initializer_list<expr*> args) { return mk_and(m, static_cast<unsigned>(args.size()), args.begin()); }
 inline app_ref mk_and(app_ref_vector const& args) { return app_ref(mk_and(args.get_manager(), args.size(), args.data()), args.get_manager()); }
 inline expr_ref mk_and(expr_ref_vector const& args) { return expr_ref(mk_and(args.get_manager(), args.size(), args.data()), args.get_manager()); }
@@ -125,6 +126,7 @@ app_ref operator+(expr_ref& a, expr_ref& b);
  */
 expr * mk_or(ast_manager & m, unsigned num_args, expr * const * args);
 app  * mk_or(ast_manager & m, unsigned num_args, app * const * args);
+inline expr * mk_or(ast_manager & m, expr* a, expr* b) { expr* args[2] = { a, b }; return mk_or(m, 2, args); }
 inline expr * mk_or(ast_manager & m, std::initializer_list<expr*> args) { return mk_or(m, static_cast<unsigned>(args.size()), args.begin()); }
 inline app_ref mk_or(app_ref_vector const& args) { return app_ref(mk_or(args.get_manager(), args.size(), args.data()), args.get_manager()); }
 inline expr_ref mk_or(expr_ref_vector const& args) { return expr_ref(mk_or(args.get_manager(), args.size(), args.data()), args.get_manager()); }