test/regress/regress1/quantifiers/issue5482-rtf-no-fv.smt2


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15

; COMMAND-LINE: --fmf-bound
; EXPECT: unsat
(set-logic AUFNIA)
(declare-fun a () Int)
(declare-fun b () (Array Int Int))
(declare-fun c () (Array Int Int))
(declare-fun d () Int)
(assert
 (exists ((e Int))
 (and (<= e 0)
  (exists ((f Int))
  (and (<= 0 f e)
   (> (select (store b 0 (select c (div a d))) f)
   (select (store b 0 (select c (div a d))) e)))))))
(check-sat)