diff --git a/src/sat/smt/fpa_solver.cpp b/src/sat/smt/fpa_solver.cpp index 590929a91..bdf224328 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)); }