summaryrefslogtreecommitdiff
path: root/test/regress/regress0/bv/fuzz07-delta.smt
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress0/bv/fuzz07-delta.smt')
-rw-r--r--test/regress/regress0/bv/fuzz07-delta.smt39
1 files changed, 0 insertions, 39 deletions
diff --git a/test/regress/regress0/bv/fuzz07-delta.smt b/test/regress/regress0/bv/fuzz07-delta.smt
deleted file mode 100644
index 50bdd4cb2..000000000
--- a/test/regress/regress0/bv/fuzz07-delta.smt
+++ /dev/null
@@ -1,39 +0,0 @@
-(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
-)))))))))))))))))))))))))))))))))
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback