From 0e78f092b5ffb4f866cbafd4fc1950363aa232c7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 7 Apr 2020 19:28:02 -0700 Subject: [PATCH] fix #3849 Signed-off-by: Nikolaj Bjorner --- src/muz/transforms/dl_mk_elim_term_ite.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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);