diff options
| author | Tim King <taking@cs.nyu.edu> | 2012-11-25 01:02:49 +0000 |
|---|---|---|
| committer | Tim King <taking@cs.nyu.edu> | 2012-11-25 01:02:49 +0000 |
| commit | c10c62d53ae784f22021cd172697eded385e5d69 (patch) | |
| tree | 1bcf419f40dd917bc43db1b47e0d402610a58c62 /test | |
| parent | 493129f815d0e45ee72ffb782632d98fc25fe2f1 (diff) | |
Adding a regression test from bug 462.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/regress0/auflia/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/auflia/error72.delta2.smt | 12 |
2 files changed, 14 insertions, 1 deletions
diff --git a/test/regress/regress0/auflia/Makefile.am b/test/regress/regress0/auflia/Makefile.am index cce2866f5..d12bb0441 100644 --- a/test/regress/regress0/auflia/Makefile.am +++ b/test/regress/regress0/auflia/Makefile.am @@ -20,7 +20,8 @@ TESTS = \ fuzz03.smt \ fuzz04.smt \ fuzz05.smt \ - a17.smt + a17.smt \ + error72.delta2.smt EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/auflia/error72.delta2.smt b/test/regress/regress0/auflia/error72.delta2.smt new file mode 100644 index 000000000..e843e0b41 --- /dev/null +++ b/test/regress/regress0/auflia/error72.delta2.smt @@ -0,0 +1,12 @@ +(benchmark fuzzsmt +:logic QF_AUFLIA +:extrafuns ((v1 Int)) +:status sat +:formula +(let (?n1 0) +(flet ($n2 (distinct v1 ?n1)) +(let (?n3 (ite $n2 v1 ?n1)) +(let (?n4 (~ ?n3)) +(flet ($n5 (>= ?n4 ?n1)) +$n5 +)))))) |