diff options
| author | Morgan Deters <mdeters@gmail.com> | 2011-07-11 16:53:50 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2011-07-11 16:53:50 +0000 |
| commit | b16e3a3187ce721e32042f241cc718529cdd0573 (patch) | |
| tree | 4d0fcb10546ccfdddb51e7eb6cfe890185a0aff2 /test/regress | |
| parent | 2ae8fae8c1e1de22c2324e5c63c5d7fd73a4582e (diff) | |
minimized example
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/regress0/arrays/Makefile.am | 1 | ||||
| -rw-r--r-- | test/regress/regress0/arrays/incorrect2.minimized.smt | 19 |
2 files changed, 20 insertions, 0 deletions
diff --git a/test/regress/regress0/arrays/Makefile.am b/test/regress/regress0/arrays/Makefile.am index 2e302f1ee..e3b30827c 100644 --- a/test/regress/regress0/arrays/Makefile.am +++ b/test/regress/regress0/arrays/Makefile.am @@ -13,6 +13,7 @@ TESTS = \ EXTRA_DIST = $(TESTS) \ incorrect1.smt \ incorrect2.smt \ + incorrect2.minimized.smt \ incorrect3.smt \ incorrect4.smt \ incorrect5.smt \ diff --git a/test/regress/regress0/arrays/incorrect2.minimized.smt b/test/regress/regress0/arrays/incorrect2.minimized.smt new file mode 100644 index 000000000..aa803d060 --- /dev/null +++ b/test/regress/regress0/arrays/incorrect2.minimized.smt @@ -0,0 +1,19 @@ +(benchmark fuzzsmt +:logic QF_AX +:extrafuns ((v3 Index)) +:extrafuns ((v4 Index)) +:extrafuns ((v2 Index)) +:status unknown +:formula +(flet ($n1 true) +(flet ($n2 (= v4 v3)) +(flet ($n3 (xor $n1 $n2)) +(flet ($n4 (distinct v2 v3)) +(let (?n5 (ite $n4 v3 v4)) +(let (?n6 (ite $n4 ?n5 v3)) +(flet ($n7 (distinct v4 ?n6)) +(flet ($n8 false) +(flet ($n9 (if_then_else $n7 $n8 $n1)) +(flet ($n10 (and $n3 $n9)) +$n10 +))))))))))) |