Levent Erkök

@ulysses4ever Turns out you were right, and this isn't actually about TH. I was able to track it to the following root-cause: If you include a file in your distribution...

This is unlikely to be implemented anytime soon; will re-open if there's an external request for the same.

Closing this; unless there's some real customer request (and help!); I doubt this'll ever happen.

4 years passed, and I doubt we have much progress here. The undefined behavior for conversions is tricky, and even the solvers do not seem to agree. Unless there's some...

z3 used to support sets via arrays mapping elements to booleans. Of course, you can still do the same, but in the past it also allowed for cardinality checking. At...

Related: https://github.com/Z3Prover/z3/issues/6548. Bottom line, z3's handling of `fpToReal` is rather weak; even constant conversions give it hard time. In my experiments, I found cvc5 to perform better for floats; so...

Rounding makes sense when the target is a floating-point number. You probably want to convert the real to a float and then compare. Take a look at https://smtlib.cs.uiowa.edu/theories-FloatingPoint.shtml. I think...

Yes; that seems to work better: ```python from z3 import * solver = Solver() x = FP('x',Float32()) solver.add(x == fpRealToFP(RNE(), RealVal(99.2), Float32())) print(solver.check()) print(solver.model()) ``` This prints: ``` sat [x...

@NikolajBjorner might still want to take a look at it, since there’s some improvements z3 can definitely do with respect to these conversions.

Update: Still observing the same memory behavior with z3 built this morning.