mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-20 02:00:22 +00:00
Code Activity

AG - unary datatypes, tester always is true.

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-09-01 09:45:56 -07:00
parent ac5b190a72
commit 46383a0811
1 changed files with 4 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/rewriter/datatype_rewriter.cpp
View file

@ -32,6 +32,10 @@ br_status datatype_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr
// simplify is_cons(nil) -> false // simplify is_cons(nil) -> false
// //
SASSERT(num_args == 1); SASSERT(num_args == 1);
if (m_util.get_datatype_num_constructors(args[0]->get_sort()) == 1) {
result = m().mk_true();
return BR_DONE;
}
if (!is_app(args[0]) || !m_util.is_constructor(to_app(args[0]))) if (!is_app(args[0]) || !m_util.is_constructor(to_app(args[0])))
return BR_FAILED; return BR_FAILED;
if (to_app(args[0])->get_decl() == m_util.get_recognizer_constructor(f)) if (to_app(args[0])->get_decl() == m_util.get_recognizer_constructor(f))