diff options
| author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-07-06 17:10:53 +0000 |
|---|---|---|
| committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-07-06 17:10:53 +0000 |
| commit | 86eb2490a00466d5b014976fc89b813011b663eb (patch) | |
| tree | 5a9cf7efb8ba9ad356a9a4a0021400c191cd30e7 /test | |
| parent | 971681afb1c9518d232d5d234800ab5da209a222 (diff) | |
Adding Array types to SMT2 parser
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/regress0/arr1.smt2 | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/test/regress/regress0/arr1.smt2 b/test/regress/regress0/arr1.smt2 new file mode 100644 index 000000000..844f7d8e5 --- /dev/null +++ b/test/regress/regress0/arr1.smt2 @@ -0,0 +1,10 @@ +(set-logic QF_AX) +(set-info :status unsat) +(declare-sort Index 0) +(declare-sort Element 0) +(declare-fun a () (Array Index Element)) +(declare-fun i1 () Index) +(declare-fun i2 () Index) +(assert (not (=> (= i1 i2) (= (select a i1) (select a i2))))) +(check-sat) + |