diff options
| author | Clark Barrett <barrett@cs.nyu.edu> | 2012-11-14 21:54:25 +0000 |
|---|---|---|
| committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-11-14 21:54:25 +0000 |
| commit | 56013a80a76b0d46f6f8497d7570e51877dbf99d (patch) | |
| tree | 9d4ed01590a15b13b91485333fd497e26889e0c0 /test/regress/regress0/auflia/fuzz04.smt | |
| parent | b273e586629c5759dc88cd962e52a89f65b674a7 (diff) | |
bug fixes to models, array rewriter with previously failing testcases
Diffstat (limited to 'test/regress/regress0/auflia/fuzz04.smt')
| -rw-r--r-- | test/regress/regress0/auflia/fuzz04.smt | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/test/regress/regress0/auflia/fuzz04.smt b/test/regress/regress0/auflia/fuzz04.smt new file mode 100644 index 000000000..7523aae28 --- /dev/null +++ b/test/regress/regress0/auflia/fuzz04.smt @@ -0,0 +1,15 @@ +(benchmark fuzzsmt +:logic QF_AUFLIA +:extrapreds ((p1 Array Array)) +:extrafuns ((f1 Array Array Array Array)) +:extrafuns ((v3 Array)) +:status sat +:formula +(let (?n1 (f1 v3 v3 v3)) +(let (?n2 0) +(let (?n3 (store v3 ?n2 ?n2)) +(let (?n4 (f1 v3 v3 ?n3)) +(let (?n5 (f1 v3 ?n4 v3)) +(flet ($n6 (p1 ?n1 ?n5)) +$n6 +))))))) |