diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index ebb6e8c48..4ed428d02 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -587,7 +587,7 @@ class theory_lra::imp { terms[index] = n1; if (!ctx().e_internalized(n)) { app* t = to_app(n); - internalize_args(t); + VERIFY(internalize_term(to_app(n1))); mk_enode(t); theory_var v = mk_var(n); theory_var w = mk_var(n1);