assertion violation when using tester

[lynaghk]

First, thanks for Z3, it's really great!

I get this error on both 4.8.12.0 and a locally-built version of f7a2d08. Both on a Mac M1, MacOS 11.6
Reporting it, as requested =D

ASSERTION VIOLATION
File: /opt/local/var/macports/build/_opt_bblocal_var_buildworker_ports_build_ports_math_z3/z3/work/z3-z3-4.8.12/src/ast/datatype_decl_plugin.cpp
Line: 1241
UNEXPECTED CODE WAS REACHED.
4.8.12.0
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new

Input code:

(declare-datatype Signal ((A) (B)))

(declare-datatype Mapping ((NoSignal)
                           (mk-signal (get-signal Signal))))

(declare-const x Signal)

(assert ((_ is get-signal) x))

(check-sat)

[NikolajBjorner]

It is type error in the input, not handled correctly internally.

You probably want:

(declare-datatype Signal ((A) (B)))

(declare-datatype Mapping ((NoSignal)
                           (mk-signal (get-signal Signal))))

(declare-const x Mapping) 

(assert ((_ is mk-signal) x))

(check-sat)

[lynaghk]

Yep, I realized my mistake but wanted to report the crash. Looks like the fix was straightforward, I'll try digging further myself next time. Thanks for the quick fix and all of your hard work on this great tool!

[NikolajBjorner]

no problem at all. It is really helpful to have a test case when fixing the missing check.