From: Tim King <taking@cs.nyu.edu>
Date: Wed, 30 Nov 2011 20:03:00 +0000 (+0000)
Subject: Simplified bug288.smt to reflect the problem in integers better.
X-Git-Tag: cvc5-1.0.0~8371
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=70552e569ad46010ab8b00f93d1c7741bafb29b1;p=cvc5.git

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 3a2ded4e9..f63b56712 100644
--- 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))
 )