We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 3180be5 commit b0253c5Copy full SHA for b0253c5
SSA/Projects/InstCombine/TacticAuto.lean
@@ -230,7 +230,7 @@ macro "bv_bench_automata": tactic =>
230
BitVec.ofNat_eq_ofNat, BitVec.two_mul]
231
all_goals (
232
tac_bench (config := { outputType := .csv }) [
233
- "bv_normalize" : (bv_normalize; done),
+ -- "bv_normalize" : (bv_normalize; done),
234
-- "presburger" : (bv_automata_gen (config := { backend := .presburger }); done),
235
"normPresburger" : ((try (solve | bv_normalize)); (try bv_automata_gen (config := { backend := .presburger })); done),
236
-- "circuitUnverified" : (bv_automata_gen (config := { backend := .circuit_cadical_unverified /- maxIter -/ 4 }); done),
0 commit comments