summaryrefslogtreecommitdiff
path: root/test/regress/regress0/decision/error3.delta01.smt
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress0/decision/error3.delta01.smt')
-rw-r--r--test/regress/regress0/decision/error3.delta01.smt32
1 files changed, 0 insertions, 32 deletions
diff --git a/test/regress/regress0/decision/error3.delta01.smt b/test/regress/regress0/decision/error3.delta01.smt
deleted file mode 100644
index de4bccd77..000000000
--- a/test/regress/regress0/decision/error3.delta01.smt
+++ /dev/null
@@ -1,32 +0,0 @@
-(benchmark fuzzsmt
-:logic QF_AUFBV
-:extrafuns ((v1 BitVec[3]))
-:extrafuns ((a2 Array[13:3]))
-:status unsat
-:formula
-(let (?n1 bv0[3])
-(flet ($n2 (bvsgt v1 v1))
-(let (?n3 bv1[1])
-(let (?n4 bv0[1])
-(let (?n5 (ite $n2 ?n3 ?n4))
-(let (?n6 (sign_extend[2] ?n5))
-(flet ($n7 (bvslt ?n6 v1))
-(let (?n8 (ite $n7 ?n3 ?n4))
-(let (?n9 (sign_extend[2] ?n8))
-(let (?n10 bv0[13])
-(let (?n11 (select a2 ?n10))
-(let (?n12 (bvshl ?n9 ?n11))
-(flet ($n13 (= ?n1 ?n12))
-(flet ($n14 (not $n13))
-(let (?n15 (bvnot ?n8))
-(let (?n16 (zero_extend[10] ?n15))
-(let (?n17 bv0[11])
-(flet ($n18 (= ?n16 ?n17))
-(flet ($n19 (not $n18))
-(let (?n20 (repeat[2] ?n15))
-(let (?n21 (zero_extend[9] ?n20))
-(flet ($n22 (bvult ?n17 ?n21))
-(flet ($n23 (and $n19 $n22))
-(flet ($n24 (and $n14 $n23))
-$n24
-)))))))))))))))))))))))))
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback