Simplified bug288.smt to reflect the problem in integers better.

diff --git a/test/regress/regress0/bug288.smt b/test/regress/regress0/bug288.smt
index 3a2ded4e96ed8da7d327ebc47174be90cd038af2..f63b56712627f71c2cd7ed5ad03b2413434b734e 100644 (file)
--- a/test/regress/regress0/bug288.smt
+++ b/test/regress/regress0/bug288.smt
@@ -1,8 +1,8 @@
 (benchmark delta
-:logic QF_UFLIA
-:extrafuns ((f Int Int))
+:logic QF_LIA
 :extrafuns ((x Int))
+:extrafuns ((y Int))
 :status sat
 :formula
-(not (= x (f 0)))
+(not (<= x y))
 )