Regression from 4.8.11.0 on bitvec comparison

[vrthra]

The following works in 4.8.10.0

>>> v = (z3.Unit(z3.BitVec("bitvec_1", 8)) == z3.String('arg_1'))
>>> v
Unit(bitvec_1) == arg_1

But this happens form 4.8.11.0 onward

>>> import z3
>>> v = (z3.Unit(z3.BitVec("bitvec_1", 8)) == z3.String('arg_1'))
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
  File "/Users/rahul.gopinath/Books/4.8.11.0/lib/python3.10/site-packages/z3/z3.py", line 1012, in __eq__
    a, b = _coerce_exprs(self, other)
  File "/Users/rahul.gopinath/Books/4.8.11.0/lib/python3.10/site-packages/z3/z3.py", line 1185, in _coerce_exprs
    s = _coerce_expr_merge(s, b)
  File "/Users/rahul.gopinath/Books/4.8.11.0/lib/python3.10/site-packages/z3/z3.py", line 1170, in _coerce_expr_merge
    _z3_assert(False, "sort mismatch")
  File "/Users/rahul.gopinath/Books/4.8.11.0/lib/python3.10/site-packages/z3/z3.py", line 112, in _z3_assert
    raise Z3Exception(msg)
z3.z3types.Z3Exception: sort mismatch

It is not clear why.

(I want to compare a single character string to a bitvec here; so if there is a better way to do that, that would also be great).

[NikolajBjorner]

Characters are no longer 8 bit (ASCII) but Unicode as specified by SMTLIB2.

from z3 import *
v = (z3.Unit(z3.Const("bitvec_1", CharSort())) == z3.String('arg_1'))
print(v)
s = Solver()
s.add(v)
print(s.check())
print(s.model())

[vrthra]

What is the best way to extract ord() of a single char string if bitvec is no longer the internal representation?

[NikolajBjorner]

This was missing from the Python API. Also missing is a way to create a character literal. This is now added.
You can

ch = CharVal('A')
print(CharToInt(ch))
ch = Const('c', CharSort())
print(CharToInt(ch))