SMT: only set produce-unsat-cores when recording hints

[mtzguido]

This PR makes F* not set the produce-unsat-cores flag of Z3 unless we are recording hints. It is currently unconditionally enabled, which is not ideal as it makes Z3 slower. Example:

$ /bin/time z3 queries-FStar.Math.Lemmas.smt2 unsat_core=false > /dev/null
Command exited with non-zero status 1
0.57user 0.01system 0:00.58elapsed 100%CPU (0avgtext+0avgdata 39672maxresident)k
0inputs+0outputs (0major+7255minor)pagefaults 0swaps
$ /bin/time z3 queries-FStar.Math.Lemmas.smt2 unsat_core=true > /dev/null
Command exited with non-zero status 1
2.34user 0.00system 0:02.35elapsed 100%CPU (0avgtext+0avgdata 51964maxresident)k
0inputs+0outputs (0major+9023minor)pagefaults 0swaps

So almost 5x improvement on this example (and it's stable across random seeds), though the usual gain is more modest.

However, it does also affect Z3's heuristics, so this will introduce a bunch of noise and breakage in flaky proofs, so I don't think it can be merged right now. See related Z3 issue: Z3Prover/z3#7538

[mtzguido]

Updated, some parts of this (mostly cleanup) went to master already. I can't get a decent comparison over a large project due to many introduced failures. On some files there's no real difference, and on some SMT time can be much faster. But it does make me wonder if this is just happening since the run without unsat cores misses some propagations (like the example in the Z3 bug above) and then just happen to work. Thinking about this again, I really doubt that the overhead of computing the unsat cores can provide big performance gains, certainly not 2x/3x/4x, so I suspect it's the buggy behavior that is making this faster.

I would hold off on this until we get more clarity into what's happening.