From 5cfe273460e803cb9d121ae88d8c8baaf28e342d Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 22 Apr 2021 22:10:39 -0700
Subject: [PATCH] #5211

```
 (declare-fun v5 () Bool)
 (declare-fun i1 () Int)
 (declare-fun i2 () Int)
 (declare-fun i4 () Int)
 (declare-fun i5 () Int)
 (declare-fun i6 () Int)
 (declare-fun i9 () Int)
 (declare-fun i10 () Int)
 (assert (or (not (=> (= 23 i6 i4 i2 85) v5)) (<= i1 8 i9 i9 (+ (+ i1 349 i10 i6) i5)) (>= i4 782)))
 (check-sat)
```
---
 src/sat/smt/arith_internalize.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/sat/smt/arith_internalize.cpp b/src/sat/smt/arith_internalize.cpp
index 8c0f5fdd2..b49d73f0b 100644
--- a/src/sat/smt/arith_internalize.cpp
+++ b/src/sat/smt/arith_internalize.cpp
@@ -164,7 +164,7 @@ namespace arith {
         unsigned index = 0;
         while (index < terms.size()) {
             SASSERT(index >= vars.size());
-            expr* n = terms[index].get();
+            expr* n = terms.get(index);
             st.to_ensure_enode().push_back(n);
             if (a.is_add(n)) {
                 for (expr* arg : *to_app(n)) {
@@ -391,7 +391,7 @@ namespace arith {
 
     bool solver::internalize_term(expr* term) {
         if (!has_var(term))
-            internalize_def(term);
+            register_theory_var_in_lar_solver(internalize_def(term));
         return true;
     }