mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

fix #3509

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-25 02:42:30 -07:00
parent ea396a008a
commit 504a7550b3
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/opt/opt_context.cpp
View file

@ -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);