From ff3cff06b28ed5a1dafe3f64038826b8f808ce3c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 7 Sep 2019 17:53:01 +0300 Subject: [PATCH] deal with ite Signed-off-by: Nikolaj Bjorner --- src/tactic/fd_solver/smtfd_solver.cpp | 3 +++ 1 file changed, 3 insertions(+) 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()); }