search

ahumenberger / Z3.jl

Julia interface to Z3
MIT License
57 stars 7 forks source link

`hash` returns UInt32 making consts unable to be used in Dict #22

Open shashi opened 1 year ago

shashi commented 1 year ago 
julia> using Z3
WARNING: using Z3.RoundingMode in module Main conflicts with an existing identifier.

julia> ctx = Context()
Z3.ContextAllocated(Ptr{Nothing} @0x00006000010946f0)

julia> hash(Z3.real_const(ctx, "x")) |> typeof
UInt32

julia> Dict(Z3.real_const(ctx, "x") => "x")
ERROR: TypeError: in typeassert, expected UInt64, got a value of type UInt32
Stacktrace:
 [1] hashindex(key::Z3.ExprAllocated, sz::Int64)
   @ Base ./dict.jl:157
 [2] ht_keyindex2_shorthash!(h::Dict{Z3.ExprAllocated, String}, key::Z3.ExprAllocated)
   @ Base ./dict.jl:293
 [3] setindex!(h::Dict{Z3.ExprAllocated, String}, v0::String, key::Z3.ExprAllocated)
   @ Base ./dict.jl:370
 [4] Dict{Z3.ExprAllocated, String}(kv::Tuple{Pair{Z3.ExprAllocated, String}})
   @ Base ./dict.jl:84
 [5] Dict(ps::Pair{Z3.ExprAllocated, String})
   @ Base ./dict.jl:104
 [6] top-level scope
   @ REPL[16]:1