diff options
| author | Morgan Deters <mdeters@gmail.com> | 2011-05-23 21:58:12 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2011-05-23 21:58:12 +0000 |
| commit | 3f7f9df5f0c419b7f7dd39e32852161f406a441f (patch) | |
| tree | 67ae6454e4496f6370cf8236500946e2c7e926b0 /test/regress/regress0/arrays/arrays0.smt2 | |
| parent | 91656937b2188f05cdd9b42955c04e6157349285 (diff) | |
Merge from arrays2 branch.
Diffstat (limited to 'test/regress/regress0/arrays/arrays0.smt2')
| -rw-r--r-- | test/regress/regress0/arrays/arrays0.smt2 | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/test/regress/regress0/arrays/arrays0.smt2 b/test/regress/regress0/arrays/arrays0.smt2 new file mode 100644 index 000000000..652ff0bcb --- /dev/null +++ b/test/regress/regress0/arrays/arrays0.smt2 @@ -0,0 +1,22 @@ +(set-logic QF_AX) +(set-info :source | +Benchmarks used in the followin paper: +Big proof engines as little proof engines: new results on rewrite-based satisfiability procedure +Alessandro Armando, Maria Paola Bonacina, Silvio Ranise, Stephan Schulz. +PDPAR'05 +http://www.ai.dist.unige.it/pdpar05/ + + +|) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status unsat) +(declare-sort Index 0) +(declare-sort Element 0) +(declare-fun a1 () (Array Index Element)) +(declare-fun a2 () (Array Index Element)) +(declare-fun i1 () Index) +(assert (= (store a1 i1 (select a2 i1)) (store a2 i1 (select a1 i1)))) +(assert (not (= a1 a2))) +(check-sat) +(exit) |