From fc163356c3bcc6e21bbb52e0e7de719817138eb7 Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Fri, 9 Nov 2012 21:05:43 +0000
Subject: [PATCH] Test that breaks arithmetic model building due to disequality
 terms.

---
 test/regress/regress0/uflra/neq-deltacomp.smt | 14 ++++++++++++++
 1 file changed, 14 insertions(+)
 create mode 100644 test/regress/regress0/uflra/neq-deltacomp.smt

diff --git a/test/regress/regress0/uflra/neq-deltacomp.smt b/test/regress/regress0/uflra/neq-deltacomp.smt
new file mode 100644
index 000000000..4144fcb79
--- /dev/null
+++ b/test/regress/regress0/uflra/neq-deltacomp.smt
@@ -0,0 +1,14 @@
+(benchmark fuzzsmt
+:logic QF_UFLRA
+:extrafuns ((v2 Real))
+:extrafuns ((v1 Real))
+:extrafuns ((v0 Real))
+:status unknown
+:formula
+(let (?n1 (~ v1))
+(flet ($n2 (>= ?n1 v0))
+(let (?n3 1)
+(let (?n4 (ite $n2 v1 ?n3))
+(flet ($n5 (<= ?n4 v2))
+$n5
+))))))
-- 
2.30.2