diff options
| author | Morgan Deters <mdeters@gmail.com> | 2010-09-28 22:44:00 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2010-09-28 22:44:00 +0000 |
| commit | 1c2b7c593fa1c12575eb37e56a5c66a1a190ad81 (patch) | |
| tree | d3914a7c7277720ca6099731190fb50f260af826 /test/regress/regress0/uf | |
| parent | 665704ba3ec1201c536c2ffa27a4d667eab3e12c (diff) | |
fix predicate bug in UF; code cleanup in theory.cpp
Diffstat (limited to 'test/regress/regress0/uf')
| -rw-r--r-- | test/regress/regress0/uf/Makefile.am | 2 | ||||
| -rw-r--r-- | test/regress/regress0/uf/NEQ016_size5_reduced2a.smt | 14 | ||||
| -rw-r--r-- | test/regress/regress0/uf/NEQ016_size5_reduced2b.smt | 14 |
3 files changed, 30 insertions, 0 deletions
diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am index a5ab380ce..1471d8814 100644 --- a/test/regress/regress0/uf/Makefile.am +++ b/test/regress/regress0/uf/Makefile.am @@ -19,6 +19,8 @@ TESTS = \ eq_diamond1.smt \ eq_diamond14.reduced.smt \ eq_diamond14.reduced2.smt \ + NEQ016_size5_reduced2a.smt \ + NEQ016_size5_reduced2b.smt \ dead_dnd002.smt \ iso_brn001.smt \ simple.01.cvc \ diff --git a/test/regress/regress0/uf/NEQ016_size5_reduced2a.smt b/test/regress/regress0/uf/NEQ016_size5_reduced2a.smt new file mode 100644 index 000000000..8ea53b45e --- /dev/null +++ b/test/regress/regress0/uf/NEQ016_size5_reduced2a.smt @@ -0,0 +1,14 @@ +(benchmark NEQ016_size5.smt +:logic QF_UF +:extrapreds ((p4 U)) +:extrafuns ((c_4 U)) +:extrafuns ((c7 U)) +:extrafuns ((c_0 U)) +:status unsat +:formula +(and +(not (p4 c_0)) +(= c_0 c7) +(p4 c7) +) +) diff --git a/test/regress/regress0/uf/NEQ016_size5_reduced2b.smt b/test/regress/regress0/uf/NEQ016_size5_reduced2b.smt new file mode 100644 index 000000000..029506d75 --- /dev/null +++ b/test/regress/regress0/uf/NEQ016_size5_reduced2b.smt @@ -0,0 +1,14 @@ +(benchmark NEQ016_size5.smt +:logic QF_UF +:extrapreds ((p4 U)) +:extrafuns ((c_4 U)) +:extrafuns ((c7 U)) +:extrafuns ((c_0 U)) +:status unsat +:formula +(and +(not (p4 c_0)) +(p4 c7) +(= c_0 c7) +) +) |