test/regress/regress1/quantifiers/symmetric_unsat_7.smt2

   1 (set-logic AUFLIRA)
   2 (set-info :source | Example extracted from Peter Baumgartner's talk at CADE-21: Logical Engineering with Instance-Based Methods.
   3
   4 It was translated to SMT-LIB by Leonardo de Moura |)
   5 (set-info :smt-lib-version 2.6)
   6 (set-info :category "crafted")
   7 (set-info :status unsat)
   8 (declare-fun symmetric ((Array Int (Array Int Real)) Int) Bool)
   9 (declare-fun n () Int)
  10 (declare-fun a0 () (Array Int (Array Int Real)))
  11 (declare-fun e0 () Real)
  12 (declare-fun a1 () (Array Int (Array Int Real)))
  13 (declare-fun e1 () Real)
  14 (declare-fun a2 () (Array Int (Array Int Real)))
  15 (declare-fun e2 () Real)
  16 (declare-fun a3 () (Array Int (Array Int Real)))
  17 (declare-fun e3 () Real)
  18 (declare-fun a4 () (Array Int (Array Int Real)))
  19 (declare-fun e4 () Real)
  20 (declare-fun a5 () (Array Int (Array Int Real)))
  21 (declare-fun e5 () Real)
  22 (declare-fun a6 () (Array Int (Array Int Real)))
  23 (declare-fun e6 () Real)
  24 (assert (forall ((?a (Array Int (Array Int Real))) (?n Int)) (= (symmetric ?a ?n) (forall ((?i Int) (?j Int)) (=> (and (<= 1 ?i) (<= ?i ?n) (<= 1 ?j) (<= ?j ?n)) (= (select (select ?a ?i) ?j) (select (select ?a ?j) ?i)))))))
  25 (assert (symmetric a0 n))
  26 (assert (= a1 (store a0 0 (store (select a0 0) 0 e0))))
  27 (assert (= a2 (store a1 1 (store (select a1 1) 1 e1))))
  28 (assert (= a3 (store a2 2 (store (select a2 2) 2 e2))))
  29 (assert (= a4 (store a3 3 (store (select a3 3) 3 e3))))
  30 (assert (= a5 (store a4 4 (store (select a4 4) 4 e4))))
  31 (assert (= a6 (store a5 5 (store (select a5 5) 5 e5))))
  32 (assert (not (symmetric a6 n)))
  33 (check-sat)
  34 (exit)