| 187 | } |
| 188 | |
| 189 | TacticResult exec(const Goal &goal) const override { |
| 190 | dbg() << "\nApplying " << name << endl; |
| 191 | Tactic to(Z3_tactic_or_else(ctx(), |
| 192 | Tactic(Z3_tactic_try_for(ctx(), t, 10000)).t, |
| 193 | Tactic(Z3_tactic_skip(ctx())).t)); |
| 194 | return Z3_tactic_apply(ctx(), to.t, goal.goal); |
| 195 | } |
| 196 | }; |
| 197 | |
| 198 |