From de9368bab05cc29b7f151bcc1987985d1f0456fd Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 4 Nov 2022 11:25:34 -0700 Subject: [PATCH] Update expr_replacer.h --- src/ast/rewriter/expr_replacer.h | 1 + 1 file changed, 1 insertion(+) diff --git a/src/ast/rewriter/expr_replacer.h b/src/ast/rewriter/expr_replacer.h index 50831073b..c1bfabd12 100644 --- a/src/ast/rewriter/expr_replacer.h +++ b/src/ast/rewriter/expr_replacer.h @@ -38,6 +38,7 @@ public: void operator()(expr * t, expr_ref & result, proof_ref & result_pr); void operator()(expr * t, expr_ref & result); void operator()(expr_ref & t) { expr_ref s(t, m()); (*this)(s, t); } + void operator()(expr_ref_vector& v) { expr_ref t(m()); for (unsigned i = 0; i < v.size(); ++i) (*this)(v.get(i), t), v[i] = t; } virtual unsigned get_num_steps() const { return 0; } virtual void reset() = 0;