diff --git a/SSA/Projects/InstCombine/TacticAuto.lean b/SSA/Projects/InstCombine/TacticAuto.lean index 6210b919f..5645d31fc 100644 --- a/SSA/Projects/InstCombine/TacticAuto.lean +++ b/SSA/Projects/InstCombine/TacticAuto.lean @@ -300,8 +300,8 @@ macro "bv_bench": tactic => "bv_normalize" : (bv_normalize; done), "bv_decide" : (bv_decide; done), "bv_auto" : (bv_auto; done), - "bv_automata_circuit" : (bv_automata_circuit (config := { circuitSizeThreshold := 30 } ); done), - "bv_normalize_automata_circuit" : ((try (solve | bv_normalize)); (try bv_automata_circuit (config := { circuitSizeThreshold := 30 } )); done) + "bv_automata_circuit" : (bv_automata_circuit; done), + "bv_normalize_automata_circuit" : ((try (solve | bv_normalize)); (try bv_automata_circuit); done) ] try bv_auto try sorry