Skip to content

Commit 2ae4ac8

Browse files
fix build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
1 parent b60e1a2 commit 2ae4ac8

File tree

1 file changed

+3
-2
lines changed

1 file changed

+3
-2
lines changed

src/ast/rewriter/var_subst.cpp

+3-2
Original file line numberDiff line numberDiff line change
@@ -59,14 +59,15 @@ expr_ref var_subst::operator()(expr * n, unsigned num_args, expr * const * args)
5959
new_args.push_back(arg);
6060
else {
6161
unsigned idx = to_var(arg)->get_idx();
62-
expr* new_arg = m_std_order ? args[num_args - idx - 1] : args[idx];
62+
expr* new_arg = nullptr;
63+
if (idx < num_args)
64+
new_arg = m_std_order ? args[num_args - idx - 1] : args[idx];
6365
if (!new_arg)
6466
new_arg = arg;
6567
new_args.push_back(new_arg);
6668
}
6769
}
6870
result = m.mk_app(to_app(n)->get_decl(), new_args.size(), new_args.data());
69-
// verbose_stream() << result << "\n";
7071
return result;
7172
}
7273
SASSERT(is_well_sorted(result.m(), n));

0 commit comments

Comments
 (0)