(set-logic HORN)
(set-option :fp.xform.instantiate_arrays true)
(declare-fun P (Int) Bool)
(assert (P 0))
(check-sat)

[514] % z3 model_validate=true small.smt2
Array Instantiation called with parameters : enforce=0 nb_quantifier=1 slice_technique=no-slicing
Input rules = 
; rule count: 0
; predicate count: 0
; output: query!1
Output rules = 
; rule count: 0
; predicate count: 0
sat
(error "line 5 column 10: an invalid model was generated")
[515] % 
[515] % cat small.smt2
(set-logic HORN)
(set-option :fp.xform.instantiate_arrays true)
(declare-fun P (Int) Bool)
(assert (P 0))
(check-sat)
[516] %