diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index da2926429..05dc63efa 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -810,7 +810,7 @@ namespace opt { mk_simplify_tactic(m)); opt_params optp(m_params); tactic_ref tac1, tac2, tac3, tac4; - if (optp.elim_01()) { + if (optp.elim_01() && m_logic.is_null()) { tac1 = mk_dt2bv_tactic(m); tac2 = mk_lia2card_tactic(m); tac3 = mk_eq2bv_tactic(m);