summaryrefslogtreecommitdiff
path: root/test/regress/regress0/bv/fuzz08.smt
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress0/bv/fuzz08.smt')
-rw-r--r--test/regress/regress0/bv/fuzz08.smt19
1 files changed, 0 insertions, 19 deletions
diff --git a/test/regress/regress0/bv/fuzz08.smt b/test/regress/regress0/bv/fuzz08.smt
deleted file mode 100644
index e2a73db50..000000000
--- a/test/regress/regress0/bv/fuzz08.smt
+++ /dev/null
@@ -1,19 +0,0 @@
-(benchmark fuzzsmt
-:logic QF_BV
-:extrafuns ((v1 BitVec[9]))
-:status sat
-:formula
-(let (?n1 bv0[6])
-(let (?n2 bv0[9])
-(flet ($n3 (bvult ?n2 v1))
-(let (?n4 bv1[1])
-(let (?n5 bv0[1])
-(let (?n6 (ite $n3 ?n4 ?n5))
-(let (?n7 (sign_extend[5] ?n6))
-(flet ($n8 (bvsgt ?n1 ?n7))
-(let (?n9 (ite $n8 ?n4 ?n5))
-(let (?n10 (sign_extend[8] ?n9))
-(let (?n11 (bvcomp v1 ?n10))
-(flet ($n12 (= ?n9 ?n11))
-$n12
-)))))))))))))
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback