From: Liana Hadarean <lianahady@gmail.com>
Date: Mon, 8 Oct 2012 20:51:03 +0000 (+0000)
Subject: added reduced bv model failing test case
X-Git-Tag: cvc5-1.0.0~7726
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ffda058e93ac699b1649a87f15418f645bb13312;p=cvc5.git

added reduced bv model failing test case
---

diff --git a/test/regress/regress0/bv/fuzz07-delta.smt b/test/regress/regress0/bv/fuzz07-delta.smt
new file mode 100644
index 000000000..50bdd4cb2
--- /dev/null
+++ b/test/regress/regress0/bv/fuzz07-delta.smt
@@ -0,0 +1,39 @@
+(benchmark fuzzsmt
+:logic QF_BV
+:extrafuns ((v1 BitVec[2]))
+:status unknown
+:formula
+(let (?n1 bv0[8])
+(let (?n2 bv0[2])
+(let (?n3 bv0[5])
+(let (?n4 (sign_extend[3] v1))
+(flet ($n5 (= ?n3 ?n4))
+(let (?n6 bv1[1])
+(let (?n7 bv0[1])
+(let (?n8 (ite $n5 ?n6 ?n7))
+(let (?n9 (concat ?n8 ?n3))
+(let (?n10 (concat ?n2 ?n9))
+(flet ($n11 (= ?n1 ?n10))
+(flet ($n12 false)
+(let (?n13 bv0[4])
+(let (?n14 bv1[2])
+(let (?n15 (bvcomp v1 ?n14))
+(flet ($n16 (bvugt ?n15 ?n7))
+(let (?n17 (ite $n16 ?n6 ?n7))
+(let (?n18 (sign_extend[1] ?n17))
+(let (?n19 (sign_extend[2] ?n18))
+(flet ($n20 (= ?n13 ?n19))
+(flet ($n21 true)
+(let (?n22 bv0[16])
+(let (?n23 bv0[3])
+(flet ($n24 (bvsle ?n2 ?n18))
+(let (?n25 (ite $n24 ?n6 ?n7))
+(let (?n26 (zero_extend[2] ?n25))
+(flet ($n27 (distinct ?n23 ?n26))
+(let (?n28 (ite $n27 ?n6 ?n7))
+(let (?n29 (zero_extend[15] ?n28))
+(flet ($n30 (= ?n22 ?n29))
+(flet ($n31 (if_then_else $n20 $n21 $n30))
+(flet ($n32 (if_then_else $n11 $n12 $n31))
+$n32
+)))))))))))))))))))))))))))))))))