diff --git a/src/ast/ast.h b/src/ast/ast.h
index 52aca7aad..6b5e4c828 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -2211,6 +2211,7 @@ public:
     app * mk_or(expr * arg1, expr * arg2) { return mk_app(basic_family_id, OP_OR, arg1, arg2); }
     app * mk_and(expr * arg1, expr * arg2) { return mk_app(basic_family_id, OP_AND, arg1, arg2); }
     app * mk_or(expr * arg1, expr * arg2, expr * arg3) { return mk_app(basic_family_id, OP_OR, arg1, arg2, arg3); }
+    app * mk_or(expr* a, expr* b, expr* c, expr* d) { expr* args[4] = { a, b, c, d }; return mk_app(basic_family_id, OP_OR, 4, args); }
     app * mk_or(std::initializer_list<expr*> args) { return mk_app(basic_family_id, OP_OR, static_cast<unsigned>(args.size()), args.begin()); }
     app * mk_and(expr * arg1, expr * arg2, expr * arg3) { return mk_app(basic_family_id, OP_AND, arg1, arg2, arg3); }