diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-06-13 14:00:35 +0000 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-06-13 14:00:35 +0000 |
commit | be5c0f29e6be61edf6a197bd8e96cdeffaaffbc4 (patch) | |
tree | 5a53b4dab644ae284b1eccc6440606973463c400 /test/regress/regress0/decision/quant-symmetric_unsat_7.smt2 | |
parent | c6aecebe573aeed87ef0661b38af7c3cbc7d641f (diff) |
decision regressions, all but one fail
Diffstat (limited to 'test/regress/regress0/decision/quant-symmetric_unsat_7.smt2')
-rw-r--r-- | test/regress/regress0/decision/quant-symmetric_unsat_7.smt2 | 34 |
1 files changed, 34 insertions, 0 deletions
diff --git a/test/regress/regress0/decision/quant-symmetric_unsat_7.smt2 b/test/regress/regress0/decision/quant-symmetric_unsat_7.smt2 new file mode 100644 index 000000000..a4ce611fb --- /dev/null +++ b/test/regress/regress0/decision/quant-symmetric_unsat_7.smt2 @@ -0,0 +1,34 @@ +(set-logic AUFLIRA) +(set-info :source | Example extracted from Peter Baumgartner's talk at CADE-21: Logical Engineering with Instance-Based Methods.
+
+It was translated to SMT-LIB by Leonardo de Moura |) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status unsat) +(declare-fun symmetric ((Array Int (Array Int Real)) Int) Bool) +(declare-fun n () Int) +(declare-fun a0 () (Array Int (Array Int Real))) +(declare-fun e0 () Real) +(declare-fun a1 () (Array Int (Array Int Real))) +(declare-fun e1 () Real) +(declare-fun a2 () (Array Int (Array Int Real))) +(declare-fun e2 () Real) +(declare-fun a3 () (Array Int (Array Int Real))) +(declare-fun e3 () Real) +(declare-fun a4 () (Array Int (Array Int Real))) +(declare-fun e4 () Real) +(declare-fun a5 () (Array Int (Array Int Real))) +(declare-fun e5 () Real) +(declare-fun a6 () (Array Int (Array Int Real))) +(declare-fun e6 () Real) +(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))))))) +(assert (symmetric a0 n)) +(assert (= a1 (store a0 0 (store (select a0 0) 0 e0)))) +(assert (= a2 (store a1 1 (store (select a1 1) 1 e1)))) +(assert (= a3 (store a2 2 (store (select a2 2) 2 e2)))) +(assert (= a4 (store a3 3 (store (select a3 3) 3 e3)))) +(assert (= a5 (store a4 4 (store (select a4 4) 4 e4)))) +(assert (= a6 (store a5 5 (store (select a5 5) 5 e5)))) +(assert (not (symmetric a6 n))) +(check-sat) +(exit) |