From 59755dd72e270af30c301f29afbc666a58045f20 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 13 Mar 2020 11:42:25 -0700 Subject: [PATCH] fix #3260 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_utvpi_def.h | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_utvpi_def.h b/src/smt/theory_utvpi_def.h index 5612bc7c7..48414e629 100644 --- a/src/smt/theory_utvpi_def.h +++ b/src/smt/theory_utvpi_def.h @@ -546,8 +546,9 @@ namespace smt { // do not create an alias. return null_theory_var; } - for (unsigned i = 0; i < n->get_num_args(); ++i) { - mk_term(to_app(n->get_arg(i))); + for (expr* arg : *n) { + if (!ctx.e_internalized(arg)) + ctx.internalize(arg, false); } th_var target = mk_var(ctx.mk_enode(n, false, false, true)); coeffs.push_back(std::make_pair(target, rational(-1))); @@ -571,6 +572,10 @@ namespace smt { SASSERT(v != null_theory_var); } else { + for (expr* arg : *n) { + if (!ctx.e_internalized(arg)) + ctx.internalize(arg, false); + } v = mk_var(ctx.mk_enode(n, false, false, true)); // v = k: v <= k k <= v coeffs coeffs;