summaryrefslogtreecommitdiff
path: root/test/regress/regress0/aufbv/bug00.smt
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress0/aufbv/bug00.smt')
-rw-r--r--test/regress/regress0/aufbv/bug00.smt35
1 files changed, 0 insertions, 35 deletions
diff --git a/test/regress/regress0/aufbv/bug00.smt b/test/regress/regress0/aufbv/bug00.smt
deleted file mode 100644
index d662207dd..000000000
--- a/test/regress/regress0/aufbv/bug00.smt
+++ /dev/null
@@ -1,35 +0,0 @@
-(benchmark no_init_multi_member7.smt
-:logic QF_AUFBV
-:status unsat
-:extrafuns ((member_6_curr_2 BitVec[32]))
-:extrafuns ((arr_next_15 Array[32:32]))
-:extrafuns ((member_3_curr_4 BitVec[32]))
-:extrafuns ((main_0_x_3 BitVec[32]))
-:extrafuns ((member_3_curr_5 BitVec[32]))
-:extrafuns ((arr_val_8 Array[32:32]))
-:status unknown
-:formula
-(flet ($n1 true)
-(let (?n2 bv0[32])
-(let (?n3 bv1[32])
-(let (?n4 (select arr_val_8 member_6_curr_2))
-(flet ($n5 (= ?n3 ?n4))
-(let (?n6 (ite $n5 ?n3 ?n2))
-(flet ($n7 (= ?n2 ?n6))
-(let (?n8 (select arr_next_15 member_3_curr_5))
-(flet ($n9 (= ?n2 ?n8))
-(let (?n10 (select arr_next_15 ?n3))
-(flet ($n11 (= ?n10 member_3_curr_4))
-(let (?n12 (select arr_next_15 ?n2))
-(flet ($n13 (= ?n3 ?n12))
-(flet ($n14 (= ?n2 main_0_x_3))
-(flet ($n15 (= ?n3 member_3_curr_4))
-(flet ($n16 (and $n14 $n15))
-(let (?n17 (ite $n16 ?n2 member_3_curr_4))
-(flet ($n18 (= member_3_curr_5 ?n17))
-(flet ($n19 (= member_6_curr_2 ?n12))
-(let (?n20 (select arr_next_15 member_6_curr_2))
-(flet ($n21 (= ?n2 ?n20))
-(flet ($n22 (and $n7 $n9 $n11 $n13 $n18 $n19 $n1 $n21))
-$n22
-)))))))))))))))))))))))
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback