diff options
| author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-05-15 21:58:09 +0000 |
|---|---|---|
| committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-05-15 21:58:09 +0000 |
| commit | 4c26c4448ce58f003ab28c4cc1803aef6d3aba29 (patch) | |
| tree | 0689f75556269113b76985ee6ce35eb18e41cd74 /test/regress/regress0/auflia/bug336.smt2 | |
| parent | 7871d62e49f8ae6ad02793c2bd47b2b31e83ed64 (diff) | |
test cases
Diffstat (limited to 'test/regress/regress0/auflia/bug336.smt2')
| -rw-r--r-- | test/regress/regress0/auflia/bug336.smt2 | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/test/regress/regress0/auflia/bug336.smt2 b/test/regress/regress0/auflia/bug336.smt2 new file mode 100644 index 000000000..f8909c23c --- /dev/null +++ b/test/regress/regress0/auflia/bug336.smt2 @@ -0,0 +1,19 @@ +(set-logic QF_AUFLIA) +(set-info :source | This is based on an example in Section 6.2 of "A Decision +Procedure for an Extensional Theory of Arrays" by Stump, Barrett, Dill, and +Levitt. |) +(set-info :smt-lib-version 2.0) +(set-info :category "check") +(set-info :status unsat) +(set-info :notes |This benchmark is designed to require an array DP to propagate a properly entailed disjunction of equalities between shared terms.|) +(declare-fun a () (Array Int Int)) +(declare-fun b () (Array Int Int)) +(declare-fun v () Int) +(declare-fun w () Int) +(declare-fun x () Int) +(declare-fun y () Int) +(declare-fun g ((Array Int Int)) Int) +(declare-fun f (Int) Int) +(assert (and (= (store a x v) b) (= (store a y w) b) (not (= (f x) (f y))) (not (= (g a) (g b))))) +(check-sat) +(exit) |