BMC inconsistency on (supposed to be) equivalent formulas

[BFarinier]

z3 fp.engine=bmc behaves differently on these four formulas which looks equivalent to me. This is reproducible with 4.8.9, 4.8.10 and 4.8.11.

The following one is satisfiable :

(declare-datatype ListInt
 ((ConsInt (hdInt Int) (tlInt ListInt))
  (NilInt (default Int))))

(define-fun-rec length ((lst ListInt)) Int
 (match lst
  (((ConsInt hd tl) (+ 1 (length tl)))
   ((NilInt df) 0))))

(define-fun pred ((x Int) (y Int)) Bool (distinct x y))

(define-fun-rec forall_pred ((val Int) (lst ListInt)) Bool
 (match lst
  (((ConsInt hd tl) (and (pred val hd) (forall_pred val tl)))
   ((NilInt df) true))))

(declare-rel Pairwise (ListInt))

(declare-var val Int)
(declare-var lst ListInt)

(declare-var hd Int)
(declare-var tl ListInt)
(declare-var df Int)

(rule
 (=>
  (and
   (= lst (ConsInt hd tl))
   (forall_pred hd tl)
   (Pairwise tl))
  (Pairwise lst)))

(rule
 (=>
  (= lst (NilInt df))
  (Pairwise lst)))

(declare-rel Final (ListInt))

(rule
 (=>
  (and
   (= lst (ConsInt 2 (ConsInt 1 (NilInt 0))))
   (Pairwise lst)
   (> (length lst) 1))
  (Final lst)))

(query Final)

If I replace the recursive function forall_pred with a relation it results in an error :

(declare-datatype ListInt
 ((ConsInt (hdInt Int) (tlInt ListInt))
  (NilInt (default Int))))

(define-fun-rec length ((lst ListInt)) Int
 (match lst
  (((ConsInt hd tl) (+ 1 (length tl)))
   ((NilInt df) 0))))

(define-fun pred ((x Int) (y Int)) Bool (distinct x y))

(declare-rel Pairwise (ListInt))
(declare-rel ForallPred (Int ListInt))

(declare-var val Int)
(declare-var lst ListInt)

(declare-var hd Int)
(declare-var tl ListInt)
(declare-var df Int)

(rule
 (=>
  (and
   (= lst (ConsInt hd tl))
   (pred val hd)
   (ForallPred val tl))
  (ForallPred val lst)))

(rule
 (=>
  (= lst (NilInt df))
  (ForallPred val lst)))

(rule
 (=>
  (and
   (= lst (ConsInt hd tl))
   (ForallPred hd tl)
   (Pairwise tl))
  (Pairwise lst)))

(rule
 (=>
  (= lst (NilInt df))
  (Pairwise lst)))

(declare-rel Final (ListInt))

(rule
 (=>
  (and
   (= lst (ConsInt 2 (ConsInt 1 (NilInt 0))))
   (Pairwise lst)
   (> (length lst) 1))
  (Final lst)))

(query Final)

WARNING: non-linear BMC is highly inefficient
no proof associated with rule<null>;<null>:
query!0((ConsInt 2 (ConsInt 1 (NilInt 0)))) :- 
 Pairwise((ConsInt 2 (ConsInt 1 (NilInt 0)))).
(error "query failed: no proof associated with rule")
unknown

If then I merge the two rules of ForallPred with a match, it results in an assertion violation :

(declare-datatype ListInt
 ((ConsInt (hdInt Int) (tlInt ListInt))
  (NilInt (default Int))))

(define-fun-rec length ((lst ListInt)) Int
 (match lst
  (((ConsInt hd tl) (+ 1 (length tl)))
   ((NilInt df) 0))))

(define-fun pred ((x Int) (y Int)) Bool (distinct x y))

(declare-rel Pairwise (ListInt))
(declare-rel ForallPred (Int ListInt))

(declare-var val Int)
(declare-var lst ListInt)

(declare-var hd Int)
(declare-var tl ListInt)
(declare-var df Int)

(rule
 (=>
  (match lst
   (((ConsInt hd tl)
     (and
      (pred val hd)
      (ForallPred val tl)))
    ((NilInt df) true)))
   (ForallPred val lst)))

(rule
 (=>
  (and
   (= lst (ConsInt hd tl))
   (ForallPred hd tl)
   (Pairwise tl))
  (Pairwise lst)))

(rule
 (=>
  (= lst (NilInt df))
  (Pairwise lst)))

(declare-rel Final (ListInt))

(rule
 (=>
  (and
   (= lst (ConsInt 2 (ConsInt 1 (NilInt 0))))
   (Pairwise lst)
   (> (length lst) 1))
  (Final lst)))

(query Final)

ASSERTION VIOLATION
File: ../src/muz/bmc/dl_bmc_engine.cpp
Line: 1249
Failed to verify: unifier.unify_rules(*r0.get(), 0, *r2.get())

Finally if I merge the two rules of Pairwise with a match, it becomes unsatisfiable :

(declare-datatype ListInt
 ((ConsInt (hdInt Int) (tlInt ListInt))
  (NilInt (default Int))))

(define-fun-rec length ((lst ListInt)) Int
 (match lst
  (((ConsInt hd tl) (+ 1 (length tl)))
   ((NilInt df) 0))))

(define-fun pred ((x Int) (y Int)) Bool (distinct x y))

(declare-rel Pairwise (ListInt))
(declare-rel ForallPred (Int ListInt))

(declare-var val Int)
(declare-var lst ListInt)

(declare-var hd Int)
(declare-var tl ListInt)
(declare-var df Int)

(rule
 (=>
  (match lst
   (((ConsInt hd tl)
     (and
      (pred val hd)
      (ForallPred val tl)))
    ((NilInt df) true)))
   (ForallPred val lst)))

(rule
 (=>
  (match lst
   (((ConsInt hd tl)
     (and
      (= lst (ConsInt hd tl))
      (ForallPred hd tl)
      (Pairwise tl)))
    ((NilInt df) true)))
  (Pairwise lst)))

(declare-rel Final (ListInt))

(rule
 (=>
  (and
   (= lst (ConsInt 2 (ConsInt 1 (NilInt 0))))
   (Pairwise lst)
   (> (length lst) 1))
  (Final lst)))

(query Final)

[NikolajBjorner]

BMC functionality was developed well before recursive functions were available. This functionality isn't well worth supporting: you can unfold transitions incrementally and use Z3 from outside for arbitrary logic combinations. The BMC encoding for non-linear Horn clauses is also pretty naive and anything usable would need to rethink how you want to unfold an SLD resolution tree selectively.