I encountered a segmentation fault in Z3 when parsing the following smtlib2 input (already minimized with ddsmt):
(declare-fun f ((_ BitVec 1)) (_ BitVec 1))
(assert (= (_ bv0 1) (f (_ bv0 1))))
If the logic is set to e.g. QF_AUFBV the segmentation fault does not occur. I am currently using the version from the master branch commit cee7dd39444c9060186df79c2a2c7f8845de415b.
I also tried it with the current unstable branch version commit 882dbfc706db6e7f83b0673906983d21404b8a19, which has the same behaviour.