Unexpected expansion of recursive functions leading to non-termination

[CyrilFMoser]

I am trying to model a pattern match expression of Scala in Z3. With that model I then try to determine whether the pattern match is exhaustive or not.

As far as I have seen with my testing, if the pattern match is exhaustive, it is able to tell that is the case very quickly. But if it is not correct, it very often does not terminate. I would have thought that it would be way easier for it to figure out that a pattern match is not exhaustive?

This is an example of the latter case:

sealed trait T_A
sealed trait T_B
case class CC_A(a: Byte, b: (T_A,T_A)) extends T_A
case class CC_B(a: CC_A) extends T_A
case class CC_C() extends T_A
case class CC_D(a: CC_B, b: Int) extends T_B

val v_a: T_A = null
val v_b: Int = v_a match{
  case CC_A(_, (_,_)) => 0 
  case CC_B(CC_A(_, _)) => 1 
}

This is an inexhaustive pattern match with the case CC_C() missing. But even if I constrain the variable to be CC_C Z3 is not able to prove that such a type exists and simply does not terminate. (Maybe I should have waited for longer, but I feel like it should almost instantly recognize that there is an issue here).

In the statistics it says that it keeps expanding the recfun macros (ludicrous amounts). From the limited tests I can do to still get the same result, I feel like the issue is the function that determines whether an expression is matched and with it the subcase function.
I also feel like there is something weird happening with the solver strategy here, because it does not need to expand subcase more than once, as there is no subcase between CC_A / CC_B and CC_C as you can see below:

(or (= typ1 typ2)
   (and ((_ is (T_A () Type)) typ2)
        ((_ is (CC_A (Type Type Type) Type)) typ1)
        (= (CC_A_extends typ1) typ2))
   (and ((_ is (CC_A (Type Type Type) Type)) typ1)
        ((_ is (CC_A (Type Type Type) Type)) typ2)
        ((_ subcase 0) (a typ1) (a typ2))
        ((_ subcase 0) (b typ1) (b typ2)))
   (and ((_ is (T_A () Type)) typ2)
        ((_ is (CC_B (Type Type) Type)) typ1)
        (= (CC_B_extends typ1) typ2))
   (and ((_ is (CC_B (Type Type) Type)) typ1)
        ((_ is (CC_B (Type Type) Type)) typ2)
        ((_ subcase 0) (a typ1) (a typ2)))
   (and ((_ is (T_A () Type)) typ2)
        ((_ is (CC_C (Type) Type)) typ1)
        (= (CC_C_extends typ1) typ2))
   (and ((_ is (CC_C (Type) Type)) typ1) ((_ is (CC_C (Type) Type)) typ2))
   (and ((_ is (T_B () Type)) typ2)
        ((_ is (CC_D (Type Type Type) Type)) typ1)
        (= (CC_D_extends typ1) typ2))
   (and ((_ is (CC_D (Type Type Type) Type)) typ1)
        ((_ is (CC_D (Type Type Type) Type)) typ2)
        ((_ subcase 0) (a typ1) (a typ2))
        ((_ subcase 0) (b typ1) (b typ2)))
   (and ((_ is (Tuple (Type Type) Type)) typ1)
        ((_ is (Tuple (Type Type) Type)) typ2)
        ((_ subcase 0) (first typ1) (first typ2))
        ((_ subcase 0) (second typ1) (second typ2)))
   ((_ is (Wildcard () Type)) typ1)
   ((_ is (Wildcard () Type)) typ2))

Every and is simply another case for a combination of typ1 and typ2 to determine whether typ1 <: typ2. As you can see there is no case that allows CC_C to be a subtype of anything except for

1. Wildcards
2. CC_C
3. T_A
   None of the 3 are present in the pattern match. So if typ1 is constrained to be CC_C it can't be matched. This is the matches_condition:

(or ((_ subcase 0) t1 pattern_0) 
    ((_ subcase 0) t1 pattern_1))

And these are the definitions for pattern_0 and pattern_1 :

 (and ((_ is (CC_A (Type Type Type) Type)) pattern_0)
     (= (a pattern_0) Wildcard)
     ((_ is (Tuple (Type Type) Type)) (b pattern_0))
     (= (first (b pattern_0)) Wildcard)
     (= (second (b pattern_0)) Wildcard)

     ((_ is (CC_B (Type Type) Type)) pattern_1)
     ((_ is (CC_A (Type Type Type) Type)) (a pattern_1))
     (= (a (a pattern_1)) Wildcard)
     (= (b (a pattern_1)) Wildcard))

Now I would simply blame it on Z3 being unlucky, but it doesn't make sense to me that it would expand a function if it didn't have to. So I believe something has to be wrong on my end.

If it helps, this would be the entirety of the program, but I believe the most important parts are above:

(declare-datatypes ((Type 0)) (((T_A) (T_B) (CC_A (CC_A_a Type) (CC_A_b Type) (CC_A_extends Type)) (CC_B (CC_B_a Type) (CC_B_extends Type)) (CC_C (CC_C_extends Type)) (CC_D (CC_D_a Type) (CC_D_b Type) (CC_D_extends Type)) (Boolean) (Byte) (Char) (Int) (Tuple (first Type) (second Type)) (Wildcard) (Generic (name String)))))
(declare-fun pattern_1 () Type)
(declare-fun pattern_0 () Type)
(declare-fun param_0 () Type)
(declare-fun param_1 () Type)
(declare-fun param_2 () Type)

(declare-fun to_match_type () Type)
(declare-fun t1 () Type)
(define-funs-rec ( ( constructable ((x!1 Type)) Bool)
                   ( valid ((x!1 Type)) Bool)
                   ( subcase ((x!1 Type) (x!2 Type)) Bool))
                 ( (let ((a!1 (=> ((_ is CC_A) x!1)
                                  (and (constructable (CC_A_b x!1)))))
                         (a!2 (=> ((_ is CC_B) x!1)
                                  (and (constructable  (CC_B_a x!1)))))
                         (a!3 (=> ((_ is CC_D) x!1)
                                  (and (constructable  (CC_D_a x!1)))))
                         (a!4 (=> ((_ is Tuple) x!1)
                                  (and (constructable  (first x!1))
                                       (constructable  (second x!1))))))
                     (and (not ((_ is T_A) x!1))
                          (not ((_ is T_B) x!1))
                          a!1
                          a!2
                          a!3
                          a!4))
                   (let ((a!1 (and ((_ is Tuple)
                                     (CC_A_b x!1))
                                   ((_ is T_A) (first (CC_A_b x!1)))
                                   ((_ is T_A) (second (CC_A_b x!1)))))
                         (a!3 (or ((_ is Wildcard ) (CC_B_a x!1))
                                  (and ((_ is CC_A)
                                         param_1)
                                       (subcase  (CC_B_a x!1) param_1))))
                         (a!5 (and ((_ is CC_C) x!1)
                                   (not ((_ is Wildcard )
                                          (CC_C_extends x!1)))
                                   ((_ is T_A) (CC_C_extends x!1))
                                   (valid  (CC_C_extends x!1))))
                         (a!6 (or ((_ is Wildcard ) (CC_D_a x!1))
                                  (and ((_ is CC_B) param_2)
                                       (subcase  (CC_D_a x!1) param_2)))))
                   (let ((a!2 (and ((_ is CC_A) x!1)
                                   (or ((_ is Wildcard ) (CC_A_a x!1))
                                       ((_ is Byte) (CC_A_a x!1)))
                                   (or ((_ is Wildcard ) (CC_A_b x!1))
                                       a!1)
                                   (not ((_ is Wildcard )
                                          (CC_A_extends x!1)))
                                   ((_ is T_A) (CC_A_extends x!1))
                                   (valid  (CC_A_a x!1))
                                   (valid  (CC_A_b x!1))
                                   (valid  (CC_A_extends x!1))))
                         (a!4 (and ((_ is CC_B) x!1)
                                   a!3
                                   (not ((_ is Wildcard )
                                          (CC_B_extends x!1)))
                                   ((_ is T_A) (CC_B_extends x!1))
                                   (valid  (CC_B_a x!1))
                                   (valid  (CC_B_extends x!1))))
                         (a!7 (and ((_ is CC_D) x!1)
                                   a!6
                                   (or ((_ is Wildcard ) (CC_D_b x!1))
                                       ((_ is Int) (CC_D_b x!1)))
                                   (not ((_ is Wildcard )
                                          (CC_D_extends x!1)))
                                   ((_ is T_B) (CC_D_extends x!1))
                                   (valid  (CC_D_a x!1))
                                   (valid  (CC_D_b x!1))
                                   (valid  (CC_D_extends x!1)))))
                     (and (=> ((_ is CC_A) x!1) a!2)
                          (=> ((_ is CC_B) x!1) a!4)
                          (=> ((_ is CC_C) x!1) a!5)
                          (=> ((_ is CC_D) x!1) a!7))))
                   (or (= x!1 x!2)
                       (and ((_ is T_A) x!2)
                            ((_ is CC_A) x!1)
                            (= (CC_A_extends x!1) x!2))
                       (and ((_ is CC_A) x!1)
                            ((_ is CC_A) x!2)
                            (subcase  (CC_A_a x!1) (CC_A_a x!2))
                            (subcase  (CC_A_b x!1) (CC_A_b x!2)))
                       (and ((_ is T_A) x!2)
                            ((_ is CC_B) x!1)
                            (= (CC_B_extends x!1) x!2))
                       (and ((_ is CC_B) x!1)
                            ((_ is CC_B) x!2)
                            (subcase  (CC_B_a x!1) (CC_B_a x!2)))
                       (and ((_ is T_A) x!2)
                            ((_ is CC_C) x!1)
                            (= (CC_C_extends x!1) x!2))
                       (and ((_ is CC_C) x!1)
                            ((_ is CC_C) x!2))
                       (and ((_ is T_B) x!2)
                            ((_ is CC_D) x!1)
                            (= (CC_D_extends x!1) x!2))
                       (and ((_ is CC_D) x!1)
                            ((_ is CC_D) x!2)
                            (subcase  (CC_D_a x!1) (CC_D_a x!2))
                            (subcase  (CC_D_b x!1) (CC_D_b x!2)))
                       (and ((_ is Tuple) x!1)
                            ((_ is Tuple) x!2)
                            (subcase  (first x!1) (first x!2))
                            (subcase  (second x!1) (second x!2)))
                       ((_ is Wildcard ) x!1)
                       ((_ is Wildcard ) x!2))))
(assert (and ((_ is CC_A) pattern_0)
     (= (CC_A_a pattern_0) Wildcard)
     ((_ is Tuple) (CC_A_b pattern_0))
     (= (first (CC_A_b pattern_0)) Wildcard)
     (= (second (CC_A_b pattern_0)) Wildcard)
     ((_ is CC_B) pattern_1)
     ((_ is CC_A) (CC_B_a pattern_1))
     (= (CC_A_a (CC_B_a pattern_1)) Wildcard)
     (= (CC_A_b (CC_B_a pattern_1)) Wildcard)))
(assert (and ((_ is T_A) to_match_type)))
(assert ((_ is CC_C) t1))
(assert (subcase  t1 to_match_type))
(assert (valid  t1))
(assert (constructable  t1))
(assert (not (or (subcase  t1 pattern_0) (subcase  t1 pattern_1))))
(check-sat)