John Bender

Yep this is correct, just a leftover from modifying the original. The commented term is there for comparison.

Sorry, I took "Do not worry about making it go fast/slow" to mean that I shouldn't worry about including both in the program. The following will work with the `quant`...

Ah and to answer your question about our use case, we have many queries that involve a large top level conjunct and the overhead demonstrated here is roughly 3x. The...

That's the correct way to run it but I'm getting a significantly different timing result. What version of z3 do you have? I'm running 4.12.2.

Tried with 4.13.3 and same result. If I do a profile build would it be helpful to attach that here?

I'm compiling within an existing stack project. This suggests a question about what flags we are using and we have the following in our `stack.yaml` ``` ghc-options: - -threaded -...

I suppose but separately I can't understand why the non-quantified version would run so much faster on your machine? I'm working on a 3ghz Xeon with 100gb of ram and...

Could you try printing the transcript for both examples (potentially with a much smaller term count) and running Z3 on it directly to see how long the solving there takes?...

I'm not sure of what to make of the 14 seconds of overhead for the quant example and the 4 seconds of overhead for the conjunct example beyond our original...

Attached are both strace profiles and basic profiling information for both quant and no quant runs. A few notes: 1. Profiling with ghc profiling enabled does not include system call...