Set all Z3 options regardless of Z3 version

This returns to the behavior prior to PR dafny-lang#3233.

It seems that the case_split change makes "time travelling triggers"
more likely: dafny-lang#3362

And, although the arith_solver change sped up verification of some
programs, it seems that it slowed down more programs.

I'd still like to leave the version detection logic in, though, since
the language server uses it, and since I think other parts of the CLI
will likely use it soon.

Source/DafnyCore/DafnyOptions.cs

@@ -1162,11 +1162,14 @@ private void SetZ3Options(Version z3Version) {
  SetZ3Option("smt.qi.eager_threshold", "100"); // TODO: try lowering
  SetZ3Option("smt.delay_units", "true");
 
- if (z3Version is not null && z3Version.CompareTo(new Version(4, 8, 5)) <= 0) {
- // These options tend to help with Z3 4.8.5 but hurt with newer versions of Z3.
- SetZ3Option("smt.case_split", "3");
- SetZ3Option("smt.arith.solver", "2");
- }
+ // This option helps avoid "time travelling triggers".
+ // See: https://github.com/dafny-lang/dafny/discussions/3362
+ SetZ3Option("smt.case_split", "3");
+
+ // This option tends to lead to the best all-around arithmetic
+ // performance, though some programs can be verified more quickly
+ // (or verified at all) using a different solver.
+ SetZ3Option("smt.arith.solver", "2");
 
  if (DisableNLarith || 3 <= ArithMode) {
  SetZ3Option("smt.arith.nl", "false");