test/regress/regress0/bug484.smt2

   1 ; COMMAND-LINE: --lang=smt2.5
   2 ; EXPECT: sat
   3
   4 ; Preamble  --------------
   5 (set-logic ALL)
   6 (set-info :status sat)
   7 (declare-datatypes () ((UNIT (Unit))))
   8 (declare-datatypes () ((BOOL (Truth) (Falsity))))
   9
  10 ; Decls     --------------
  11 (declare-sort A 0)
  12 (declare-sort B 0)
  13 (declare-sort C 0)
  14 (declare-sort D 0)
  15 (declare-datatypes () ((E (one) (two) (three))))
  16 (declare-datatypes () ((F (four) (five) (six))))
  17 (declare-datatypes () ((G (c_G (seven BOOL)))))
  18
  19 (declare-datatypes ()
  20   ((H
  21     (c_H
  22       (foo1 BOOL)
  23       (foo2 A)
  24       (foo3 B)
  25       (foo4 B)
  26       (foo5 Int)
  27     )
  28   ))
  29 )
  30
  31 (declare-datatypes ()
  32   ((I
  33     (c_I
  34       (bar1 E)
  35       (bar2 Int)
  36       (bar3 Int)
  37       (bar4 A)
  38     )
  39   ))
  40 )
  41
  42 (declare-datatypes ()
  43   ((J
  44     (c_J
  45       (f1 BOOL)
  46       (f2 Int)
  47       (f3 Int)
  48       (f4 Int)
  49       (f5 I)
  50       (f6 B)
  51       (f7 C)
  52     )
  53   ))
  54 )
  55
  56 (declare-datatypes ()
  57   ((K
  58     (c_K
  59       (g1 BOOL)
  60       (g2 F)
  61       (g3 A)
  62       (g4 BOOL)
  63     )
  64   ))
  65 )
  66
  67 ; Var Decls --------------
  68 (declare-fun s1 () (Array A J))
  69 (declare-fun s2 () (Array A J))
  70 (declare-fun e1 () (Array A K))
  71 (declare-fun e2 () (Array A K))
  72 (declare-fun x  () A)
  73 (declare-fun y  () A)
  74 (declare-fun foo (A) A)
  75 (declare-fun bar (A) C)
  76
  77
  78 ; Asserts   --------------
  79 (assert
  80   (not
  81     (=
  82       (ite
  83         (=>
  84           (= y (g3 (select e1 x)))
  85           (=>
  86             (= s2
  87                (store
  88                  s1
  89                  y
  90                  (let ((z (select s1 y)))
  91                    (c_J
  92                      (f1 z)
  93                      (f2 z)
  94                      (- (f3 (select s1 y)) 1)
  95                      (f4 z)
  96                      (f5 z)
  97                      (f6 z)
  98                      (f7 z)
  99                    )
 100                  )
 101                )
 102             )
 103             (forall ((s A)) (= (g3 (select e2 s)) s))
 104           )
 105         )
 106        Truth
 107        Falsity
 108       )
 109       Truth
 110     )
 111   )
 112 )
 113
 114 (check-sat)