diff --git a/src/tactic/fd_solver/smtfd_solver.cpp b/src/tactic/fd_solver/smtfd_solver.cpp
index ffcd5943f..5b44b756f 100644
--- a/src/tactic/fd_solver/smtfd_solver.cpp
+++ b/src/tactic/fd_solver/smtfd_solver.cpp
@@ -275,6 +275,9 @@ namespace smtfd {
                     if (m.is_eq(a)) {
                         r = m.mk_eq(m_args.get(0), m_args.get(1));
                     }
+                    else if (m.is_ite(a)) {
+                        r = m.mk_ite(m_args.get(0), m_args.get(1), m_args.get(2));
+                    }
                     else if (bvfid == fid || bfid == fid) {
                         r = m.mk_app(a->get_decl(), m_args.size(), m_args.c_ptr());
                     }