From 03b5380a204179b479799c28f648abc4c3c707e2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 14 Dec 2021 13:39:52 -0800 Subject: [PATCH] na --- src/ast/rewriter/var_subst.h | 1 + 1 file changed, 1 insertion(+) diff --git a/src/ast/rewriter/var_subst.h b/src/ast/rewriter/var_subst.h index 84318c9b5..e9d39740d 100644 --- a/src/ast/rewriter/var_subst.h +++ b/src/ast/rewriter/var_subst.h @@ -48,6 +48,7 @@ public: Otherwise, (VAR 0) is stored in the first position, (VAR 1) in the second, and so on. */ expr_ref operator()(expr * n, unsigned num_args, expr * const * args); + inline expr_ref operator()(expr* n, expr* arg) { return (*this)(n, 1, &arg); } inline expr_ref operator()(expr * n, expr_ref_vector const& args) { return (*this)(n, args.size(), args.data()); } inline expr_ref operator()(expr * n, var_ref_vector const& args) { return (*this)(n, args.size(), (expr*const*)args.data()); } inline expr_ref operator()(expr * n, app_ref_vector const& args) { return (*this)(n, args.size(), (expr*const*)args.data()); }