ahumenberger

> The questions is whether we want to treat a polynomial with `Integer` coefficients as a polynomial in ℤ[x]. If I'm explicitly constructing a Polynomial{true, Int} I would expect it...

Any progress here? I'm experiencing the same problem with Julia 1.0.4 on Ubuntu 18.04 LTS and 19.04. ```julia julia> Conda.list() [ Info: Downloading miniconda installer ... --2019-10-02 08:53:06-- https://repo.continuum.io/miniconda/Miniconda3-latest-Linux-x86.sh Resolving...

> Any progress here? I'm experiencing the same problem with Julia 1.0.4 on Ubuntu 18.04 LTS and 19.04. I solved my issue. It turned out that I had a 32-bit...

Thanks for the hint! `Z3.ctx` is actually a function coming from the Z3 API, and `ctx` is often used as a variable name. I was thinking about aliasing `Z3.ctx` by...

I guess the easiest solution is to use a lambda expression to return an `unsigned long` for the hash function in https://github.com/Z3Prover/z3/blob/master/src/api/julia/z3jl.cpp. Something like the following should work I think:...

The Z3 repo contains examples for the C++ API which you can translate into Julia code. For instance, the optimization example from https://github.com/Z3Prover/z3/blob/7eb05dd952a2f5de1d4be09436a97651c85dba18/examples/c%2B%2B/example.cpp#L1024 would translate to the following Julia code:...

Sorry for the delay. I was pretty busy the last few weeks. The issue Z3Prover/z3#4728 is closed, is this still relevant?

It seems as some objects are garbage collected before they are used within the call to `add(solver, c == 1)`. For me it works if I expand the lifetime of...

`(root-obj (+ (* 64 (^ x 2)) (- 63)) 1)` is an algebraic number representing the first root of the polynomial 64*x^2 - 63. You can get a real approximation...

These need to be added to https://github.com/Z3Prover/z3/blob/master/src/api/julia/z3jl.cpp, which lists types, methods, etc. from the Z3 C++ API which should be exposed in Julia. Apparently formal and exists are still missing...