Adding a failing UFLIA benchmark corresponding to bug #288.

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index e564b567ad75d56a55c3a9ad77218a961ed5878b..7128c50887fc05dfeb44553492ba362e55b6398f 100644 (file)
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -94,6 +94,7 @@ BUG_TESTS = \
        bug187.smt2 \
        bug220.smt2 \
        bug239.smt \
+       bug288.smt \
        buggy-ite.smt2
 
 TESTS =        $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS)

diff --git a/test/regress/regress0/bug288.smt b/test/regress/regress0/bug288.smt
new file mode 100644 (file)
index 0000000..3a2ded4
--- /dev/null
+++ b/test/regress/regress0/bug288.smt
@@ -0,0 +1,8 @@
+(benchmark delta
+:logic QF_UFLIA
+:extrafuns ((f Int Int))
+:extrafuns ((x Int))
+:status sat
+:formula
+(not (= x (f 0)))
+)