Zvonimir Rakamaric

So I finally run our large-scale experiments and did a comparison between old arithmetic solver and the new one in the nightly build. Right now the differences seem to be...

Oh, you are right. Let me double-check this. It indeed looks weird that they are so similar. I'll get back to you.

Is there debug info that Z3 prints out that tells me which arithmetic solver it is running?

Ok, I got it. So scatter plot generation is buggy for some reason. We haven't been using it that much recently, and I guess some of our recent updates broke...

Got it. If there is a particular one you are maybe interested in (or a few of them), I can generate the query for you.

Sorry for the delay. Let me run our regressions on the latest nightly release.

@NikolajBjorner Quick question. I don't see a nightly release for Ubuntu. I am looking here: https://github.com/Z3Prover/z3/releases/tag/Nightly Am I missing something? Should I build it from source on Ubuntu!? Thanks!

Why did you choose these names: `half_pi`, `two_pi`, `pi`, and `e_const`? They are not uniform since `e` has `const` added to the end of it. I suspect you did that...

How about `exp`? http://www.cplusplus.com/reference/cmath/exp/

I think I like `exp1` the best.