dReal and z3 giving different bounds

[zenna]

Running the following example gives different bounds for z3 and dReal

A = ifelse(Sigma.flipsmt(0.4),Sigma.discreteuniformsmt(0,1),1)
prob(A==1)

julia> prob(A==1;solver=Sigma.z3)
Reached Max iterations - 1000
[0.7990226745605464 0.800918579101562]

julia> prob(A==1;solver=Sigma.dreal)
Reached Max iterations - 1000
[0.5937499999999996 0.8038940429687462]

The difference (they should be the same) could be due to a bug (prob in dReal). Or it could be a fundamental property of the delta relaxation, which I've been avoiding thinking about.