diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-04-11 16:31:03 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-04-11 16:31:03 +0000 |
commit | d01d291be3213368985f28d0072905c4f033d5ff (patch) | |
tree | 8524a2b6a00c012221ecca9266c3ab9fb11989ed /test/regress/regress0/arrays | |
parent | 889853e225687dfef36b15ca1dccf74682e0fd66 (diff) |
merge from arrays-clark branch
Diffstat (limited to 'test/regress/regress0/arrays')
-rw-r--r-- | test/regress/regress0/arrays/Makefile.am | 4 | ||||
-rw-r--r-- | test/regress/regress0/arrays/x2.smt | 17 | ||||
-rw-r--r-- | test/regress/regress0/arrays/x3.smt | 46 |
3 files changed, 66 insertions, 1 deletions
diff --git a/test/regress/regress0/arrays/Makefile.am b/test/regress/regress0/arrays/Makefile.am index b112d1129..5a18658d5 100644 --- a/test/regress/regress0/arrays/Makefile.am +++ b/test/regress/regress0/arrays/Makefile.am @@ -25,7 +25,9 @@ TESTS = \ incorrect8.minimized.smt \ incorrect9.smt \ incorrect10.smt \ - incorrect11.smt + incorrect11.smt \ + x2.smt \ + x3.smt EXTRA_DIST = $(TESTS) \ bug272.smt \ diff --git a/test/regress/regress0/arrays/x2.smt b/test/regress/regress0/arrays/x2.smt new file mode 100644 index 000000000..c043e88b9 --- /dev/null +++ b/test/regress/regress0/arrays/x2.smt @@ -0,0 +1,17 @@ +(benchmark read5.smt +:logic QF_AX +:status unsat +:extrafuns ((a Index)) +:extrafuns ((S Array)) +:extrafuns ((SS Array)) +:status unknown +:formula +(flet ($n1 (= S SS)) +(let (?n2 (select S a)) +(let (?n3 (store SS a ?n2)) +(flet ($n4 (= S ?n3)) +(flet ($n5 true) +(flet ($n6 (if_then_else $n1 $n4 $n5)) +(flet ($n7 (not $n6)) +$n7 +)))))))) diff --git a/test/regress/regress0/arrays/x3.smt b/test/regress/regress0/arrays/x3.smt new file mode 100644 index 000000000..ff070f142 --- /dev/null +++ b/test/regress/regress0/arrays/x3.smt @@ -0,0 +1,46 @@ +(benchmark fuzzsmt +:logic QF_AX +:status sat +:extrafuns ((v4 Index)) +:extrafuns ((v2 Index)) +:extrafuns ((v3 Index)) +:extrafuns ((v1 Array)) +:extrafuns ((v6 Element)) +:extrafuns ((v0 Array)) +:extrafuns ((v5 Element)) +:status unknown +:formula +(let (?n1 (store v1 v3 v6)) +(flet ($n2 (distinct ?n1 v0)) +(flet ($n3 (= v4 v2)) +(flet ($n4 true) +(let (?n5 (store v1 v4 v6)) +(let (?n6 (select ?n5 v2)) +(let (?n7 (ite $n4 ?n6 v6)) +(let (?n8 (select v1 v3)) +(let (?n9 (ite $n3 ?n7 ?n8)) +(flet ($n10 (distinct ?n8 ?n8)) +(let (?n11 (ite $n10 v6 ?n6)) +(let (?n12 (ite $n2 ?n9 ?n11)) +(flet ($n13 (= v6 ?n12)) +(flet ($n14 (distinct ?n8 v5)) +(let (?n15 (ite $n2 v1 v0)) +(let (?n16 (ite $n14 v1 ?n15)) +(flet ($n17 (distinct ?n5 ?n16)) +(flet ($n18 (and $n13 $n17)) +(flet ($n19 (distinct v0 ?n5)) +(let (?n20 (ite $n19 v2 v4)) +(flet ($n21 (= v3 v2)) +(flet ($n22 (= v0 v0)) +(flet ($n23 (= v6 ?n8)) +(flet ($n24 false) +(flet ($n25 (= ?n6 ?n8)) +(let (?n26 (ite $n25 v3 v2)) +(let (?n27 (ite $n24 v4 ?n26)) +(let (?n28 (ite $n23 v3 ?n27)) +(let (?n29 (ite $n22 ?n28 v4)) +(let (?n30 (ite $n21 v3 ?n29)) +(flet ($n31 (distinct ?n20 ?n30)) +(flet ($n32 (or $n18 $n31)) +$n32 +))))))))))))))))))))))))))))))))) |