diff options
| author | Morgan Deters <mdeters@gmail.com> | 2011-03-30 21:53:15 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2011-03-30 21:53:15 +0000 |
| commit | b04d7ee960729bcde8677be3682a2d64789f825b (patch) | |
| tree | 77fd43bfddfac2cbae0ce0565b4328ecbc3fec72 /test/regress/regress0/uf | |
| parent | af976fc656590dbbbfbcdfa45da5dbdab51f4c1c (diff) | |
improve recent low-coverage complaints
Diffstat (limited to 'test/regress/regress0/uf')
| -rw-r--r-- | test/regress/regress0/uf/Makefile.am | 1 | ||||
| -rw-r--r-- | test/regress/regress0/uf/euf_simp09.tim.smt | 14 |
2 files changed, 15 insertions, 0 deletions
diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am index 54d89aaaa..e288a01d2 100644 --- a/test/regress/regress0/uf/Makefile.am +++ b/test/regress/regress0/uf/Makefile.am @@ -12,6 +12,7 @@ TESTS = \ euf_simp06.smt \ euf_simp08.smt \ euf_simp09.smt \ + euf_simp09.tim.smt \ euf_simp10.smt \ euf_simp11.smt \ euf_simp12.smt \ diff --git a/test/regress/regress0/uf/euf_simp09.tim.smt b/test/regress/regress0/uf/euf_simp09.tim.smt new file mode 100644 index 000000000..309090507 --- /dev/null +++ b/test/regress/regress0/uf/euf_simp09.tim.smt @@ -0,0 +1,14 @@ +% COMMAND-LINE: --uf tim +% EXPECT: unsat +% EXIT: 20 +(benchmark euf_simp9.smt + + :status unsat + :difficulty { unknown } + :category { crafted } + :logic QF_UF + :extrasorts (A) + :extrafuns ((x A)) + :extrafuns ((f A A)) + :formula (let (?cvc_1 (f (f x))) (let (?cvc_0 (f (f ?cvc_1))) (not (implies (and (= ?cvc_0 x) (= (f (f ?cvc_0)) x)) (= ?cvc_1 x))))) +) |