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); } }