Timeout with simple datatype example

[hiroshi-unno]

In Z3 version 4.13.3, the following datatype example causes a timeout in satisfiability checking.

(declare-datatypes ((A4_Box<List> 0)
    (A3_List 0)
    (A1_Tuple<Box<Int>-Box<Box<List>>> 0)
    (A5_Box<Box<List>> 0)
    (A0_Box<Int> 0))
   (
    ((box<List> (box_current<List> A3_List)))
    ((List.Nil) (List.Cons (_getList.Cons A1_Tuple<Box<Int>-Box<Box<List>>>)))
    ((tuple<Box<Int>-Box<Box<List>>> (tuple_proj<Box<Int>-Box<Box<List>>>.0 A0_Box<Int>) (tuple_proj<Box<Int>-Box<Box<List>>>.1 A5_Box<Box<List>>)))
    ((box<Box<List>> (box_current<Box<List>> A4_Box<List>)))
    ((box<Int> (box_current<Int> Int)))
   ))
(declare-fun |#tvar3358| () A3_List)
(declare-fun |#tvar3356| () A1_Tuple<Box<Int>-Box<Box<List>>>)
(assert (and (not (= (List.Cons |#tvar3356|) |#tvar3358|))
     (not (= List.Nil |#tvar3358|))))

(check-sat)
(exit)

Simplifying the datatype slightly returns "sat" immediately, suggesting a potential bug.