diff options
Diffstat (limited to 'test/regress/regress0')
| -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) +) +) |