Spacer CHC solver and pattern-matching

[BFarinier]

I am facing the following issue when using pattern-matching with the Spacer CHC solver:

(declare-datatype OptionInt
 ((SomeInt (valueInt Int))
  (NoneInt)))

(define-fun getValueDefault ((opt OptionInt) (default Int)) Int
 (match opt
  (((SomeInt int) int)
   (NoneInt default))))

(declare-var opt1 OptionInt)
(declare-var opt2 OptionInt)

(declare-var default Int)

(declare-rel equalOptionInt (OptionInt OptionInt))

(rule
 (=>
  (= (getValueDefault opt1 default) (getValueDefault opt2 default))
  (equalOptionInt opt1 opt2)))

(query equalOptionInt)

(error "query failed: Uninterpreted 'valueInt' in <null>:
equalOptionInt(#1,#0) :- 
 (= (ite ((_ is (SomeInt (Int) OptionInt)) (:var 1))
        (valueInt (:var 1))
        (:var 2))
   (ite ((_ is (SomeInt (Int) OptionInt)) (:var 0))
        (valueInt (:var 0))
        (:var 2))).
")
unknown

As far as I understand, pattern-matching in getValueDefault is deconstructed as an if then else in which selectors appear. But according to #3070 selectors are partially-defined, leading to the error. This is regrettable as the original pattern-matching was fully-specified.

Do you think there is a chance that the Spacer CHC solver could support fully-specified pattern-matching? I know that I could use the workaround detailed in #3070, but my real case involves nested pattern-matching, and doing so will result in the introduction of hundreds variables, an extent that I would like to avoid...

[gernst]

Maybe a related comment (not sure if this behavior is intended though):

(set-logic HORN)

(declare-datatype OptionInt
 ((SomeInt (valueInt Int))
  (NoneInt)))

(declare-const v OptionInt)
(assert ((_ is SomeInt) v))

results in (error "line 8 column 25: invalid use of indexed identifier, unknown builtin function is"), but works fine with the default logic (or ALL).