fix #4623

Signed-off-by: Nikolaj Bjorner <[email protected]>
Z3Prover · Aug 11, 2020 · 7fc4653 · 7fc4653
1 parent 9f7e80c
commit 7fc4653
Showing 1 changed file with 5 additions and 0 deletions.
diff --git 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;