Assertion Violation at ../src/ast/datatype_decl_plugin.cpp

[brutalsavage]

Hi all

Description: ASSERTION VIOLATION

small code small.smt2 to reproduce:

(declare-sort D)
(declare-datatypes () ((MyOption (Some (elem D)) None)))
(declare-fun f (MyOption D) D)
(assert (not (= (f (Some (elem 1))) (f (Some (elem 2))))))
(check-sat)
(exit)

output

ASSERTION VIOLATION
File: ../src/ast/datatype_decl_plugin.cpp
Line: 676
is_datatype(s)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
A

Command: running z3 (e6ea815) with debug build z3 small.smt2