diff options
Diffstat (limited to 'test/regress/regress0/arrays/x3.smtv1.smt2')
-rw-r--r-- | test/regress/regress0/arrays/x3.smtv1.smt2 | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/test/regress/regress0/arrays/x3.smtv1.smt2 b/test/regress/regress0/arrays/x3.smtv1.smt2 new file mode 100644 index 000000000..3b2257fec --- /dev/null +++ b/test/regress/regress0/arrays/x3.smtv1.smt2 @@ -0,0 +1,14 @@ +(set-option :incremental false) +(set-info :status sat) +(set-info :status unknown) +(set-logic QF_AUF) +(declare-sort Index 0) +(declare-sort Element 0) +(declare-fun v4 () Index) +(declare-fun v2 () Index) +(declare-fun v3 () Index) +(declare-fun v1 () (Array Index Element)) +(declare-fun v6 () Element) +(declare-fun v0 () (Array Index Element)) +(declare-fun v5 () Element) +(check-sat-assuming ( (let ((_let_0 (distinct (store v1 v3 v6) v0))) (let ((_let_1 (store v1 v4 v6))) (let ((_let_2 (select _let_1 v2))) (let ((_let_3 (select v1 v3))) (or (and (= v6 (ite _let_0 (ite (= v4 v2) (ite true _let_2 v6) _let_3) (ite (distinct _let_3 _let_3) v6 _let_2))) (distinct _let_1 (ite (distinct _let_3 v5) v1 (ite _let_0 v1 v0)))) (distinct (ite (distinct v0 _let_1) v2 v4) (ite (= v3 v2) v3 (ite (= v0 v0) (ite (= v6 _let_3) v3 (ite false v4 (ite (= _let_2 _let_3) v3 v2))) v4)))))))) )) |