diff options
Diffstat (limited to 'test/regress/regress0/aufbv/bug00.smt')
-rw-r--r-- | test/regress/regress0/aufbv/bug00.smt | 35 |
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 -))))))))))))))))))))))) |