Spacer: Timeout with simple array example

[mmsbrggr]

Hi everyone,

I am trying to use Spacer to verify programs that contain arrays/maps, when I noticed for some seemingly simple benchmarks Spacer gets stuck in a loop. Using different parameters for spacer and z3 did not help. I distilled a minimal simple benchmark that Spacer struggles with. Is there anything I can do get an answer for this and similar benchmarks (like combination of special parameters, different encoding, custom invariants, ...)?

(set-logic HORN)
(set-option :fp.spacer.q3.use_qgen true)
(set-option :fp.spacer.ground_pobs false)
(declare-fun INV ((Array Int Bool) Int) Bool)

; initial state
(assert (forall ((set (Array Int Bool))
         (element Int))
  (=> (and (= ((as const (Array Int Bool)) false) set)
           (= 0 element))
      (INV set element))))

; transition: set stays the same; inc element
(assert (forall ((set (Array Int Bool))
         (element Int)
         (set_ (Array Int Bool))
         (element_ Int))
  (=> (and (INV set element)
           (= set_ set)
           (= element_ (+ 1 element))
           )
      (INV set_ element_))))

; property: element not in set
(assert (forall ((set (Array Int Bool))
         (element Int))
  (=> (and (INV set element))
      (not (select set element)))))

(check-sat)

The benchmark encodes the following transition system: The state consists of an array (called set) and integer (called element). set is initialized to be an array mapping every integer to false, and element to 0. There is a single (symbolic) transition incrementing element (set remains the same). The query is given by the property that select set element is false, which must hold as set is always the array mapping every integer to false.

Any help is appreciated!