Problem with Hashing `Z3.ExprAllocated` in Julia 1.6

[yangky11]

Hi,

I have the following error when trying to add a Z3 expr to a Set. The code works in Julia 1.5 but breaks in Julia 1.6. It looks like the hash function for Z3 expr returns UInt32, but Julia 1.6 requires UInt64.

  TypeError: in typeassert, expected UInt64, got a value of type UInt32
  Stacktrace:
    [1] hashindex(key::Z3.ExprAllocated, sz::Int64)
      @ Base ./dict.jl:169
    [2] ht_keyindex2!(h::Dict{Z3.ExprAllocated, Nothing}, key::Z3.ExprAllocated)
      @ Base ./dict.jl:310
    [3] setindex!(h::Dict{Z3.ExprAllocated, Nothing}, v0::Nothing, key::Z3.ExprAllocated)
      @ Base ./dict.jl:383
    [4] push!(s::Set{Z3.ExprAllocated}, x::Z3.ExprAllocated)
      @ Base ./set.jl:57

[Philipp15b]

I'm new to Julia, so I don't know if there's a better solution using overloading than the following. Rename the hash method of the ast Z3 bindings to hash32 and then add a new hash implementation for AST objects in Julia code.

--- src/api/julia/z3jl.cpp
+++ src/api/julia/z3jl.cpp
@@ -136,7 +136,7 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m)
     TYPE_OBJ(ast)
         .constructor<context &>()
         .constructor<ast const &>()
-        .MM(ast, hash)
+        .method("hash32", &ast::hash)
         .method("string", &ast::to_string);
 
     m.method("isequal", &eq);

hash(x::T, h::UInt) where {T <: Ast} = hash(UInt(hash32(x)), h)

A simpler solution would be to patch the hash method in Z3 directly to return an unsigned long instead of unsigned, but then the upper bits of the hash value would be empty.

[ahumenberger]

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:

 .method("hash", [](ast &a) { return (unsigned long)a.hash(); })