diff options
| author | Tim King <taking@cs.nyu.edu> | 2012-11-26 17:30:44 +0000 |
|---|---|---|
| committer | Tim King <taking@cs.nyu.edu> | 2012-11-26 17:30:44 +0000 |
| commit | c3ca3d8c58cc9954f8ad190e1e2dedbcbb5372f0 (patch) | |
| tree | 4830fb02118a499da8cb62aaec06b16919e0d05a /test | |
| parent | 2a731b9164bb178f1232a9af0babc7dd84450cea (diff) | |
Removing DioSolver::acceptableOriginalNodes(). This assertion was too strong, and was broken by r4620. This commit resolves bug463. Adding a previously triggering test case.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/regress0/auflia/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/auflia/x2.smt | 28 |
2 files changed, 30 insertions, 1 deletions
diff --git a/test/regress/regress0/auflia/Makefile.am b/test/regress/regress0/auflia/Makefile.am index d12bb0441..cc4a1556f 100644 --- a/test/regress/regress0/auflia/Makefile.am +++ b/test/regress/regress0/auflia/Makefile.am @@ -21,7 +21,8 @@ TESTS = \ fuzz04.smt \ fuzz05.smt \ a17.smt \ - error72.delta2.smt + error72.delta2.smt \ + x2.smt EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/auflia/x2.smt b/test/regress/regress0/auflia/x2.smt new file mode 100644 index 000000000..3566d9858 --- /dev/null +++ b/test/regress/regress0/auflia/x2.smt @@ -0,0 +1,28 @@ +(benchmark fuzzsmt +:logic QF_AUFLIA +:extrafuns ((v4 Array)) +:extrafuns ((f0 Int Int)) +:extrapreds ((p0 Int Int Int)) +:status sat +:formula +(let (?n1 0) +(flet ($n2 (p0 ?n1 ?n1 ?n1)) +(let (?n3 1) +(let (?n4 (ite $n2 ?n3 ?n1)) +(flet ($n5 (< ?n1 ?n4)) +(flet ($n6 (p0 ?n3 ?n1 ?n1)) +(let (?n7 (ite $n6 ?n3 ?n1)) +(let (?n8 (ite $n5 ?n7 ?n3)) +(flet ($n9 (< ?n1 ?n8)) +(flet ($n10 true) +(let (?n11 3) +(let (?n12 (f0 ?n1)) +(let (?n13 (* ?n11 ?n12)) +(let (?n14 (select v4 ?n1)) +(flet ($n15 (> ?n13 ?n14)) +(flet ($n16 (xor $n10 $n15)) +(flet ($n17 false) +(flet ($n18 (implies $n16 $n17)) +(flet ($n19 (and $n9 $n18)) +$n19 +)))))))))))))))))))) |