From 86c35bc7c1d98dc4e5919933b1e52e37297a6489 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 1 Dec 2019 17:10:21 -0800
Subject: [PATCH] fix #2763

---
 src/smt/theory_lra.cpp | 11 +++++++++--
 src/smt/theory_lra.h   |  2 ++
 2 files changed, 11 insertions(+), 2 deletions(-)

diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 64e233069..845f28df2 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -974,6 +974,12 @@ public:
         m_arith_eq_adapter.new_diseq_eh(v1, v2);
     }
 
+    void apply_sort_cnstr(enode* n, sort*) {
+        if (!th.is_attached_to_var(n)) {
+            mk_var(n->get_owner(), false);
+        }
+    }
+
     void push_scope_eh() {
         TRACE("arith", tout << "push\n";);
         m_scopes.push_back(scope());
@@ -1393,7 +1399,6 @@ public:
         
         if (v == null_theory_var || 
             v >= static_cast<theory_var>(m_theory_var2var_index.size())) {
-            TRACE("arith", tout << "Variable v" << v << " not internalized\n";);
             return rational::zero();
         }
             
@@ -1402,7 +1407,6 @@ public:
             return m_variable_values[vi];
         
         if (!m_solver->is_term(vi)) {
-            TRACE("arith", tout << "not a term v" << v << "\n";);
             return rational::zero();
         }
         
@@ -3591,6 +3595,9 @@ bool theory_lra::use_diseqs() const {
 void theory_lra::new_diseq_eh(theory_var v1, theory_var v2) {
     m_imp->new_diseq_eh(v1, v2);
 }
+void theory_lra::apply_sort_cnstr(enode* n, sort* s) {
+    m_imp->apply_sort_cnstr(n, s);
+}
 void theory_lra::push_scope_eh() {
     theory::push_scope_eh();
     m_imp->push_scope_eh();
diff --git a/src/smt/theory_lra.h b/src/smt/theory_lra.h
index 56370899e..f3f7c8e55 100644
--- a/src/smt/theory_lra.h
+++ b/src/smt/theory_lra.h
@@ -75,6 +75,8 @@ namespace smt {
 
         void reset_eh() override;
 
+        void apply_sort_cnstr(enode * n, sort * s) override;
+
         void init_model(model_generator & m) override;
         
         model_value_proc * mk_value(enode * n, model_generator & mg) override;