From eed3fa6d49270acba4e12554917a069a810120f3 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 15 Jan 2025 18:54:50 -0800
Subject: [PATCH] add case for ite

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/dyn_ack.cpp | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/src/smt/dyn_ack.cpp b/src/smt/dyn_ack.cpp
index 006f40b22..ed440ee75 100644
--- a/src/smt/dyn_ack.cpp
+++ b/src/smt/dyn_ack.cpp
@@ -431,7 +431,6 @@ namespace smt {
         justification * js = nullptr;
         if (m.proofs_enabled())
             js = alloc(dyn_ack_cc_justification, n1, n2);
-        verbose_stream() << "dynack-clause\n";
         clause * cls = m_context.mk_clause(lits.size(), lits.data(), js, CLS_TH_LEMMA, del_eh);
         if (!cls) {
             dealloc(del_eh);
@@ -491,8 +490,6 @@ namespace smt {
         ctx.mark_as_relevant(eq1);
         ctx.mark_as_relevant(eq2);
         ctx.mark_as_relevant(eq3);
-        verbose_stream() << "dynack-transitivity\n";
-        clause * cls = ctx.mk_clause(lits.size(), lits.data(), js, CLS_TH_LEMMA, del_eh);
         if (!cls) {
             dealloc(del_eh);
             return;