It seems like Z3 returns an error if get-value is called with an empty list which in turn triggers an unreachable call. Instead of doing that, the library should catch the problem when get_value is called so that the user gets a meaningful error message.
It seems like Z3 returns an error if
get-valueis called with an empty list which in turn triggers an unreachable call. Instead of doing that, the library should catch the problem whenget_valueis called so that the user gets a meaningful error message.