From 7fc4653e4783db45c862979154ccf383d267ef47 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 11 Aug 2020 14:08:53 -0700 Subject: [PATCH] fix #4623 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_datatype.cpp | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp index 004f69bd11e..9e7bfad2b1f 100644 --- a/src/smt/theory_datatype.cpp +++ b/src/smt/theory_datatype.cpp @@ -856,6 +856,11 @@ namespace smt { enode * n = get_enode(v); sort * dt = m.get_sort(n->get_owner()); var_data * d = m_var_data[v]; + if (d->m_recognizers.empty()) { + theory_var w = recognizer->get_arg(0)->get_th_var(get_id()); + SASSERT(w != null_theory_var); + add_recognizer(w, recognizer); + } CTRACE("datatype", d->m_recognizers.empty(), ctx.display(tout);); SASSERT(!d->m_recognizers.empty()); literal_vector lits;