From 9e391cf8cd7b496f57f3c6c2128ab1111ea1a4b5 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Sat, 7 Feb 2026 13:40:48 +0000 Subject: [PATCH] Changes before error encountered Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/ast/ast_util.h | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/ast/ast_util.h b/src/ast/ast_util.h index e23bc6d34..b245f9b15 100644 --- a/src/ast/ast_util.h +++ b/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 const& args) { return mk_and(m, args.size(), args.data()); } inline expr * mk_and(ast_manager & m, ptr_buffer 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 args) { return mk_and(m, static_cast(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 args) { return mk_or(m, static_cast(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()); }