Wrong model for simple list CHC

[reinerfx]

Dear Philipp Ruemmer,

it seems to me eldarica is returning a model to this CHC instance that cannot be correct:

( declare-datatypes ( ( list_tp 0 ) ) ( ( empty_list ( list ( hd Int ) ( tail list_tp ) ) ) ) )

(declare-fun p ( list_tp ) Bool)

(assert (p empty_list))

(assert (forall ( ( l list_tp ) ) (=> (p l) (p l))))

(assert (=> (p ( list 1 empty_list ) ) false))

(check-sat)

~/eldarica/eld -ssol min.smt2 
sat
(
    (define-fun p ((A list_tp)) Bool true)
)

[pruemmer]

Great catch! Indeed, there was a bug in solution generation related to data types, which should be fixed in the latest commit.