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

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

diff --git a/src/smt/dyn_ack.cpp b/src/smt/dyn_ack.cpp
index ed440ee75..84b28a7a5 100644
--- a/src/smt/dyn_ack.cpp
+++ b/src/smt/dyn_ack.cpp
@@ -490,6 +490,7 @@ namespace smt {
         ctx.mark_as_relevant(eq1);
         ctx.mark_as_relevant(eq2);
         ctx.mark_as_relevant(eq3);
+        clause* cls = ctx.mk_clause(lits.size(), lits.data(), js, CLS_TH_LEMMA, del_eh);
         if (!cls) {
             dealloc(del_eh);
             return;