mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

fix #4623

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-08-11 14:08:53 -07:00
parent 9f7e80c440
commit 7fc4653e47
1 changed files with 5 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/smt/theory_datatype.cpp
View file

@ -856,6 +856,11 @@ namespace smt {
enode * n = get_enode(v); enode * n = get_enode(v);
sort * dt = m.get_sort(n->get_owner()); sort * dt = m.get_sort(n->get_owner());
var_data * d = m_var_data[v]; 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);); CTRACE("datatype", d->m_recognizers.empty(), ctx.display(tout););
SASSERT(!d->m_recognizers.empty()); SASSERT(!d->m_recognizers.empty());
literal_vector lits; literal_vector lits;