diff --git a/src/muz/transforms/dl_mk_elim_term_ite.cpp b/src/muz/transforms/dl_mk_elim_term_ite.cpp index 7e0356e7e..d340e750a 100644 --- a/src/muz/transforms/dl_mk_elim_term_ite.cpp +++ b/src/muz/transforms/dl_mk_elim_term_ite.cpp @@ -165,7 +165,8 @@ namespace datalog { head = ground(head); fml2 = m.mk_implies(body, head); - SASSERT(!has_term_ite(fml2)); + if (has_term_ite(fml2)) + return false; app_ref_vector consts(m); collect_uninterp_consts(fml2, consts); fml2 = mk_forall(m, consts.size(), consts.c_ptr(), fml2);