From 2ae4ac8d0a24b6542306737501bcc2679e34fcd2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 4 Oct 2024 08:38:52 -0700 Subject: [PATCH] fix build Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/var_subst.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/ast/rewriter/var_subst.cpp b/src/ast/rewriter/var_subst.cpp index 711ca2b51..820a235d8 100644 --- a/src/ast/rewriter/var_subst.cpp +++ b/src/ast/rewriter/var_subst.cpp @@ -59,14 +59,15 @@ expr_ref var_subst::operator()(expr * n, unsigned num_args, expr * const * args) new_args.push_back(arg); else { unsigned idx = to_var(arg)->get_idx(); - expr* new_arg = m_std_order ? args[num_args - idx - 1] : args[idx]; + expr* new_arg = nullptr; + if (idx < num_args) + new_arg = m_std_order ? args[num_args - idx - 1] : args[idx]; if (!new_arg) new_arg = arg; new_args.push_back(new_arg); } } result = m.mk_app(to_app(n)->get_decl(), new_args.size(), new_args.data()); - // verbose_stream() << result << "\n"; return result; } SASSERT(is_well_sorted(result.m(), n));