From ed3f8a52e6f010d14f9bfca39331dec8cf22fee8 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 4 Aug 2021 14:05:22 -0700
Subject: [PATCH] #5454

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

diff --git a/src/sat/smt/fpa_solver.cpp b/src/sat/smt/fpa_solver.cpp
index 590929a91bd..bdf22432829 100644
--- a/src/sat/smt/fpa_solver.cpp
+++ b/src/sat/smt/fpa_solver.cpp
@@ -226,6 +226,9 @@ namespace fpa {
                     add_unit(eq_internalize(wrapped, cc_args));
                     add_units(mk_side_conditions());
                 }
+                else if (m.is_ite(n)) {
+                    // pass
+                }
                 else 
                     add_unit(eq_internalize(m_converter.unwrap(wrapped, n->get_sort()), n));                
             }