klab-prove: stop passing custom tactic to z3

[asymmetric]

This could be a possible source of indeterminism, and we're anyway not
sure if we still need it.

Cf. discussion at #305.

Ci at https://buildbot.dapp.ci/#/builders/2/builds/592.

[asymmetric]

According to Z3's (help-tactic), (or-else <tactic>) tries each tactic in sequence until one succeeds, so the global Z3 timeout would trigger before any of the other tactics after the first one could have a chance to run, assuming that the global timeout affects tactic execution.

So this seems to be a good change, but not one that would trigger any semantic change.

/cc @ehildenb

[asymmetric]

@MrChico @mhhf @livnev why do we need to set the global z3 timeout? Does Z3 have a default that's way too high?

If this is the default value, then yes, it's slightly too high.

[asymmetric]

Turns out K sets the default for --z3-impl-timeout to 5000ms.

[mhhf]

As lev said in the discussion we used it to work around a nondetermenistic arichmetic solving - some seeds returned instantly the unsat result, some timed out. By trying 3 seeds in sequence we ensured that the probability of timing out a correct result is low.
However we did this long time ago with complicated nonlinear math (rpow) and it wouldn't surprise me if we don't need this tactic in most cases. Even an expression timing out is a rare occurence with K&Z3 so if everything is passing without it. If everything is fine without this tactic, lets remove it.
However I would note it in some README/TROUBLESHOOTING log that z3 misbehaves sometimes and one needs to be mindful about this, in special when edeting the smt-prelude

[mhhf]

On the other hand, why do you dislike it being in place in general?

[asymmetric]

On the other hand, why do you dislike it being in place in general?

@mhhf because noone really knows if it works (IIUC the global timeout makes it useless since it prevents Z3 from trying the other tactics) or if we still need it.

I would be open to leave it if we find a legitimate use for it, even if it's only useful sometimes. But if we're just not sure and we might maybe need it and so on, then I think it should go, and we put it back when we're sure we need it.

[mhhf]

true, global timeout breaks it
i'm ok with removing it then