diff options
| author | Morgan Deters <mdeters@gmail.com> | 2011-07-11 18:48:16 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2011-07-11 18:48:16 +0000 |
| commit | 4c428c8f74ae913f05287c0595c8887c31089520 (patch) | |
| tree | ab3041c59d6d8700e96c623675a1570208c6374f /test/regress/regress0/arrays | |
| parent | b16e3a3187ce721e32042f241cc718529cdd0573 (diff) | |
if running in QF_AX, equalities over terms of uninterpreted sort go to arrays, as well as pre-registration of free constants of uninterpreted sort, etc..
Diffstat (limited to 'test/regress/regress0/arrays')
| -rw-r--r-- | test/regress/regress0/arrays/Makefile.am | 7 | ||||
| -rw-r--r-- | test/regress/regress0/arrays/incorrect2.minimized.smt | 2 | ||||
| -rw-r--r-- | test/regress/regress0/arrays/incorrect8.minimized.smt | 20 |
3 files changed, 25 insertions, 4 deletions
diff --git a/test/regress/regress0/arrays/Makefile.am b/test/regress/regress0/arrays/Makefile.am index e3b30827c..b7a60917b 100644 --- a/test/regress/regress0/arrays/Makefile.am +++ b/test/regress/regress0/arrays/Makefile.am @@ -8,9 +8,7 @@ TESTS = \ arrays1.smt2 \ arrays2.smt2 \ arrays3.smt2 \ - arrays4.smt2 - -EXTRA_DIST = $(TESTS) \ + arrays4.smt2 \ incorrect1.smt \ incorrect2.smt \ incorrect2.minimized.smt \ @@ -20,10 +18,13 @@ EXTRA_DIST = $(TESTS) \ incorrect6.smt \ incorrect7.smt \ incorrect8.smt \ + incorrect8.minimized.smt \ incorrect9.smt \ incorrect10.smt \ incorrect11.smt +EXTRA_DIST = $(TESTS) + #if CVC4_BUILD_PROFILE_COMPETITION #else #TESTS += \ diff --git a/test/regress/regress0/arrays/incorrect2.minimized.smt b/test/regress/regress0/arrays/incorrect2.minimized.smt index aa803d060..6bb3bbfd8 100644 --- a/test/regress/regress0/arrays/incorrect2.minimized.smt +++ b/test/regress/regress0/arrays/incorrect2.minimized.smt @@ -3,7 +3,7 @@ :extrafuns ((v3 Index)) :extrafuns ((v4 Index)) :extrafuns ((v2 Index)) -:status unknown +:status unsat :formula (flet ($n1 true) (flet ($n2 (= v4 v3)) diff --git a/test/regress/regress0/arrays/incorrect8.minimized.smt b/test/regress/regress0/arrays/incorrect8.minimized.smt new file mode 100644 index 000000000..18067e654 --- /dev/null +++ b/test/regress/regress0/arrays/incorrect8.minimized.smt @@ -0,0 +1,20 @@ +(benchmark fuzzsmt +:logic QF_AX +:extrafuns ((v4 Index)) +:extrafuns ((v3 Index)) +:extrafuns ((v5 Element)) +:extrafuns ((v1 Array)) +:status unknown +:formula +(let (?n1 (store v1 v4 v5)) +(let (?n2 (select ?n1 v3)) +(let (?n3 (select v1 v3)) +(flet ($n4 (distinct ?n2 ?n3)) +(let (?n5 (ite $n4 v4 v3)) +(let (?n6 (store ?n1 v4 v5)) +(let (?n7 (select ?n6 v3)) +(flet ($n8 (= ?n2 ?n7)) +(let (?n9 (ite $n8 v3 v4)) +(flet ($n10 (distinct ?n5 ?n9)) +$n10 +))))))))))) |