mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-18 02:16:40 +00:00
Code Activity

c is non-null

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-07-02 10:57:54 -07:00
parent 75678fc2c2
commit bb100a40d5
1 changed files with 2 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/ast/datatype_decl_plugin.cpp
View file

@ -1106,9 +1106,8 @@ namespace datatype {
symbol r; symbol r;
// Use O(1) lookup instead of O(n) linear search // Use O(1) lookup instead of O(n) linear search
constructor* c = dd.get_constructor_by_name(con); constructor* c = dd.get_constructor_by_name(con);
if (c) { SASSERT(c);
r = c->recognizer(); r = c->recognizer();
}
parameter ps[2] = { parameter(con), parameter(r) }; parameter ps[2] = { parameter(con), parameter(r) };
d = m.mk_func_decl(fid(), OP_DT_RECOGNISER, 2, ps, 1, &datatype); d = m.mk_func_decl(fid(), OP_DT_RECOGNISER, 2, ps, 1, &datatype);
SASSERT(d); SASSERT(d);