Spacer unsoundness regarding CHCs involving inductively defined datatypes

[coord-e]

Spacer returns unsat for the following input, which suggests a soundness bug. I expect Spacer to timeout on this input, as the expected model of p1 is an inductively defined function, which, as far as I know, is not handled by the current Spacer.

; spacer_bug_1.smt2
(set-logic HORN)
(declare-datatypes ((A0_List 0)) (((List.Cons (_getList.Cons.0 Int) (_getList.Cons.1 A0_List)) (List.Nil))))

(declare-fun p1 (Int A0_List) Bool)

(assert (forall ((A A0_List) (B Int) (C Int))
       (=> (and (p1 B A) (p1 C A)) (= B C))
    ))
(assert (forall ((A A0_List))
  (=> (= A List.Nil) (p1 1 A))))
(assert (forall ((A A0_List) (B Int) (D A0_List) (E Int) (F A0_List))
       (=> (and (p1 B D) (p1 B F) (= A (List.Cons (- E B) F))) (p1 E A))
    ))

(check-sat)

$ z3 fp.engine=spacer spacer_bug_1.smt2
unsat

Spacer gives unknown for this input when I supply fp.print_certificate=true or fp.validate=true, which also suggests a potential bug.

$ z3 fp.engine=spacer fp.print_certificate=true spacer_bug_1.smt2
unknown

$ z3 fp.engine=spacer fp.validate=true spacer_bug_1.smt2
unknown

$ z3 fp.engine=spacer fp.validate=true -v:3 spacer_bug_1.smt2
(snip)
spacer: could not validate a proof step
unknown

https://gist.github.com/coord-e/68f8524df93df5cd07477baf089119fd#file-spacer_bug_1_validate_true_v_3-log

We have an inductively defined model for p1 that satisfies the constraints.

(define-fun-rec p1 ((x Int) (y A0_List)) Bool
  (ite (= y List.Nil) (= x 0)
    (p1 (- x (_getList.Cons.0 y)) (_getList.Cons.1 y))
  )
)

As a side note, this CHC is derived from the verification of the following program. p1 represents the relationship between the input and output of the acc function.

enum List {
  Cons(i32, Box<List>),
  Nil,
}

fn acc(la: &List) -> i32 {
  match la {
    List::Cons(x, la2) => *x + acc(la2),
    List::Nil => 1,
  }
}

fn main() {
  let la = rand();
  let n = acc(&la);
  let r = acc(&la);
  assert!(r == n);
}

Environment

$ z3 --version
Z3 version 4.13.0 - 64 bit

[hgvk94]

Thanks for the detailed report. Taking a look ...