CVC4 performance issue with --fmf-bound

[muchang]

For this formula, CVC4 without fmf-bound gives a result quickly, while CVC4 hangs using fmf-bound. It is likely a performance issue.

[581] % time cvc4 -q small.smt2
unsat
real  0m0.087s
user  0m0.053s
sys   0m0.004s
[582] % 
[582] % timeout -s 9 30 cvc4 --fmf-bound -q small.smt2
Killed
[583] % 
[583] % cat small.smt2
(declare-fun a () Int)
(declare-fun b () (Array Int Int))
(declare-fun c () Int)
(declare-fun d () Int)
(assert (> (select b 0) (select b 1)))
(assert (forall ((e Int)) (=> (<= 0 e (- a d)) (forall ((f Int)) (=> (<= (+ d 1) f) (<= (select b e) (select b f)))))))
(assert (exists ((h Int)) (and (<= 0 h c) (exists ((i Int)) (let ((g (store (store b 0 (select b 1)) 1 (select b 0)))) (and (<= (+ d 1) i) (> (select g h) (select g i))))))))
(assert (= a (+ d c)))
(check-sat)
[584] %

Commit: 36af095

[ajreynol]

This is expected behavior, --fmf-bound is worse for "UNSAT" instances.

Internal note: --fmf-inst-engine also does not solve this.

Transferring to cvc4-projects.