mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-26 15:53:41 +00:00
Code Activity

fix regression

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-02-02 06:16:06 -08:00
parent 937b61fc88
commit cc001ad682
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/rewriter/enum2bv_rewriter.cpp
View file

@ -99,7 +99,7 @@ struct enum2bv_rewriter::imp {
} }
else if (m_dt.is_recognizer(f) && reduce_arg(args[0], a0)) { else if (m_dt.is_recognizer(f) && reduce_arg(args[0], a0)) {
unsigned idx = m_dt.get_recognizer_constructor_idx(f); unsigned idx = m_dt.get_recognizer_constructor_idx(f);
a1 = value2bv(idx, a0->get_sort()); a1 = value2bv(idx, args[0]->get_sort());
result = m.mk_eq(a0, a1); result = m.mk_eq(a0, a1);
return BR_DONE; return BR_DONE;
} }