From be5c0f29e6be61edf6a197bd8e96cdeffaaffbc4 Mon Sep 17 00:00:00 2001
From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Wed, 13 Jun 2012 14:00:35 +0000
Subject: decision regressions, all but one fail

---
 .../decision/uflia-xs-09-16-3-4-1-5.delta03.smt    | 45 ++++++++++++++++++++++
 1 file changed, 45 insertions(+)
 create mode 100644 test/regress/regress0/decision/uflia-xs-09-16-3-4-1-5.delta03.smt

(limited to 'test/regress/regress0/decision/uflia-xs-09-16-3-4-1-5.delta03.smt')

diff --git a/test/regress/regress0/decision/uflia-xs-09-16-3-4-1-5.delta03.smt b/test/regress/regress0/decision/uflia-xs-09-16-3-4-1-5.delta03.smt
new file mode 100644
index 000000000..6f65e83ec
--- /dev/null
+++ b/test/regress/regress0/decision/uflia-xs-09-16-3-4-1-5.delta03.smt
@@ -0,0 +1,45 @@
+(benchmark mathsat
+:logic QF_UFLIA
+:extrafuns ((fmt_length Int))
+:extrafuns ((fmt1 Int))
+:extrafuns ((arg1 Int))
+:extrafuns ((select_format Int Int))
+:status sat
+:formula
+(let (?n1 1)
+(let (?n2 (+ ?n1 fmt1))
+(let (?n3 (select_format ?n2))
+(flet ($n4 (= ?n1 ?n3))
+(let (?n5 (select_format arg1))
+(let (?n6 0)
+(flet ($n7 (= ?n5 ?n6))
+(flet ($n8 (and $n4 $n7))
+(let (?n9 7)
+(let (?n10 (select_format ?n9))
+(flet ($n11 (= ?n1 ?n10))
+(let (?n12 (select_format ?n6))
+(flet ($n13 (= ?n1 ?n12))
+(let (?n14 (select_format ?n1))
+(flet ($n15 (= ?n1 ?n14))
+(flet ($n16 (or $n13 $n15))
+(let (?n17 5)
+(let (?n18 (select_format ?n17))
+(flet ($n19 (= ?n6 ?n18))
+(flet ($n20 (or $n16 $n19))
+(let (?n21 6)
+(let (?n22 (select_format ?n21))
+(flet ($n23 (= ?n6 ?n22))
+(flet ($n24 (or $n20 $n23))
+(flet ($n25 (or $n11 $n24))
+(let (?n26 9)
+(flet ($n27 (= ?n26 fmt_length))
+(let (?n28 2)
+(let (?n29 (- fmt1 ?n28))
+(flet ($n30 (= arg1 ?n29))
+(flet ($n31 (< fmt1 fmt_length))
+(flet ($n32 (and $n30 $n31))
+(flet ($n33 (and $n27 $n32))
+(flet ($n34 (and $n25 $n33))
+(flet ($n35 (and $n8 $n34))
+$n35
+))))))))))))))))))))))))))))))))))))
-- 
cgit v1.2.3