deal with ite

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Sep 7, 2019 · ff3cff0 · ff3cff0
1 parent c476c4a
commit ff3cff0
Showing 1 changed file with 3 additions and 0 deletions.
diff --git 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());
                     }