From d53e30ecbeca52875ee290da14cfe8fee49cedd6 Mon Sep 17 00:00:00 2001
From: Arie Gurfinkel <arie.gurfinkel@uwaterloo.ca>
Date: Fri, 10 Apr 2020 21:09:36 -0400
Subject: [PATCH] finished fix for #3849 by converting assert into trace

---
 src/muz/transforms/dl_mk_elim_term_ite.cpp | 2 +-
 1 file changed, 1 insertion(+), 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 218d64d0f..1005f7667 100644
--- a/src/muz/transforms/dl_mk_elim_term_ite.cpp
+++ b/src/muz/transforms/dl_mk_elim_term_ite.cpp
@@ -172,7 +172,7 @@ namespace datalog {
         rw(body);
 
         fml2 = m.mk_implies(body, ground(r.get_head()));
-        SASSERT(!has_term_ite(fml2));
+        CTRACE("dl", has_term_ite(fml2), tout << "Rule has term-ite after elimination. Giving up\n";);
         if (has_term_ite(fml2))
             return false;
         app_ref_vector consts(m);