assertion violation z3

[silvio-ghilardi]

the following message occurred while running a file of a student of mine (the student carried out an assignment solving it in a personal way) . The student file is attached below with no editing from my side.

ASSERTION VIOLATION
File: ../src/ast/datatype_decl_plugin.cpp
Line: 1295
UNEXPECTED CODE WAS REACHED.
Z3 4.12.6.0

========================================
exercise3_3.txt