From f646c9ac11d24c6e2236be7e2658c100edcfb69d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 4 Dec 2019 10:45:17 +0300 Subject: [PATCH] fix #2780 --- src/smt/theory_lra.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 21f70ac8d..9e7a3a5ba 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -976,7 +976,8 @@ public: void apply_sort_cnstr(enode* n, sort*) { if (!th.is_attached_to_var(n)) { - mk_var(n->get_owner(), false); + theory_var v = mk_var(n->get_owner(), false); + get_var_index(v); } }