hoice get stuck during preprocessing

[naokikob]

hoice (v1.10.0) gets stuck during pre-processing for the following input:

(set-logic HORN)
(declare-datatypes ((IList 0)) (((insert (head Int) (tail IList)) (nil))))

(declare-fun X (Int IList ) Bool)
(declare-fun size (IList Int) Bool)

(assert (forall ((x Int)) (size nil 0)))
(assert (forall ((x Int) (ls IList) (n Int))
	(=> (size ls n) (size (insert x ls) (+ n 1)))))
	
(assert (forall ((x Int)(ls IList)) (=> (and (X  x  ls) (<=  x 0 )) false)))
(assert (forall ((x Int)(ls IList)) (=> (and (X  x  ls) (=  (head ls) 0 ) ) (X  (- x 1) (tail ls)))))
(assert (forall ((m Int) (n Int) (ls IList)) (=> (and (size ls n) (>=  m n)) (X  m  ls))))
(check-sat)

Log:

koba@koba-PC:~$ hoice --version
hoice 1.10.0

koba@koba-PC:~$ hoice -v -v -v foo.smt2
; Running top pre-processing
; running simplify
;   simplifying clause #4 (terms_changed: true)
;     propagation...
;     pruning...
;     trivial?
;     redundancy check...
;     split disj...
;     done
;   simplifying clause #3 (terms_changed: true)
;     propagation...
;     pruning...
;     trivial?
;     redundancy check...
;     split disj...
;     done
;   simplifying clause #2 (terms_changed: true)
;     propagation...
;     pruning...
;     trivial?
;     redundancy check...
;     split disj...
;     done
;   simplifying clause #1 (terms_changed: true)
;     propagation...
;     pruning...
;     trivial?
;     redundancy check...
;     split disj...
;     done
;   simplifying clause #0 (terms_changed: true)
;     propagation...
;     pruning...
;     trivial?
;     redundancy check...
;     split disj...
;     done
; simplify: did nothing
; running arg_reduce
;     rm_args (2)
;     to keep {
;       X: v_0 v_1
;       size: v_0 v_1
;     }
; arg_reduce: did nothing
; running one_rhs
; one_rhs: did nothing
; running one_lhs
; one_lhs: did nothing
; running fun_preds
;   working on size
;     working on clause #0
;     working on clause #1
;     checking 6 invariants...
;       not an invariant: (>= (* (- 1) v_1) 1)
;       confirmed invariant: (>= v_1 0)
;       not an invariant: (not (= v_1 0))
;       not an invariant: (= v_1 0)
;       not an invariant: (>= v_1 1)
;       not an invariant: (>= (* (- 1) v_1) 0)
;     discovered 1 invariant(s)
;     all branches are exclusive
;     checking they're exhaustive
;     branches are exhaustive
;   simplifying clause #2 (terms_changed: true)
;     propagation...
;     pruning...
;     trivial?
  C-c C-c

It seems

self.is_clause_trivial(clause)

on line 439 of instance/pre_instance.rs gets stuck.

[AdrienChampion]

The issue is that hoice attempts to reconstruct predicates as functions during pre-processing. Z3 does not seem to like this at all and loops (seemingly) forever.

You can get an answer on these clauses with the --fun_preds off (hidden) option.

I would not expect hoice/z3 to get stuck on these clauses despite fun_preds, but I would need more time to investigate.