diff options
Diffstat (limited to 'test')
20 files changed, 1420 insertions, 6 deletions
diff --git a/test/regress/regress0/aufbv/Makefile b/test/regress/regress0/aufbv/Makefile new file mode 100644 index 000000000..7dd17882f --- /dev/null +++ b/test/regress/regress0/aufbv/Makefile @@ -0,0 +1,8 @@ +topdir = ../../../.. +srcdir = test/regress/regress0/aufbv + +include $(topdir)/Makefile.subdir + +# synonyms for "check" +.PHONY: test +test: check diff --git a/test/regress/regress0/aufbv/Makefile.am b/test/regress/regress0/aufbv/Makefile.am index f9ec6b474..9b9820258 100644 --- a/test/regress/regress0/aufbv/Makefile.am +++ b/test/regress/regress0/aufbv/Makefile.am @@ -9,7 +9,10 @@ endif # If a test shouldn't be run in e.g. competition mode, # put it below in "TESTS +=" TESTS = \ - bug00.smt + bug00.smt \ + bug338.smt2 \ + try5_small_difret_functions_wp_su.set_char_quoting.il.wp.delta01.smt \ + wchains010ue.delta01.smt EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/aufbv/no_init_multi_delete14.smt b/test/regress/regress0/aufbv/no_init_multi_delete14.smt new file mode 100644 index 000000000..06071cd32 --- /dev/null +++ b/test/regress/regress0/aufbv/no_init_multi_delete14.smt @@ -0,0 +1,670 @@ +(benchmark no_init_multi_delete14.smt + :source { +The benchmarks come from Bounded Model Checking of software. +Contributed by Lorenzo Platania (c1009@unige.it). +} + :status unknown + :difficulty { unknown } + :category { industrial } + :logic QF_AUFBV + :extrafuns ((main_0_head_0 BitVec[32])) + :extrafuns ((main_0_head_1 BitVec[32])) + :assumption +(= main_0_head_1 bv0[32]) + :extrafuns ((arr_val_0 Array[32:32])) + :extrafuns ((arr_val_1 Array[32:32])) + :assumption +(= arr_val_1 (store arr_val_0 main_0_head_1 bv0[32])) + :extrafuns ((arr_next_0 Array[32:32])) + :extrafuns ((arr_next_1 Array[32:32])) + :assumption +(= arr_next_1 (store arr_next_0 main_0_head_1 (bvneg bv1[32]))) + :extrafuns ((main_0_curr_0 BitVec[32])) + :extrafuns ((main_0_curr_1 BitVec[32])) + :assumption +(= main_0_curr_1 main_0_head_1) + :extrafuns ((main_0_i_0 BitVec[32])) + :extrafuns ((main_0_i_1 BitVec[32])) + :assumption +(= main_0_i_1 bv1[32]) + :extrafuns ((main_0_tmp_0 BitVec[32])) + :extrafuns ((main_0_tmp_1 BitVec[32])) + :assumption +(= main_0_tmp_1 (ite (bvult main_0_i_1 bv13[32]) bv1[32] main_0_tmp_0)) + :extrafuns ((arr_val_2 Array[32:32])) + :assumption +(= arr_val_2 (ite (bvult main_0_i_1 bv13[32]) (store arr_val_1 main_0_tmp_1 main_0_i_1) arr_val_1)) + :extrafuns ((arr_next_2 Array[32:32])) + :assumption +(= arr_next_2 (ite (bvult main_0_i_1 bv13[32]) (store arr_next_1 main_0_curr_1 main_0_tmp_1) arr_next_1)) + :extrafuns ((main_0_curr_2 BitVec[32])) + :assumption +(= main_0_curr_2 (ite (bvult main_0_i_1 bv13[32]) (select arr_next_2 main_0_curr_1) main_0_curr_1)) + :extrafuns ((arr_next_3 Array[32:32])) + :assumption +(= arr_next_3 (ite (bvult main_0_i_1 bv13[32]) (store arr_next_2 main_0_tmp_1 (bvneg bv1[32])) arr_next_2)) + :extrafuns ((main_0_temp_i_0 BitVec[32])) + :extrafuns ((main_0_temp_i_1 BitVec[32])) + :assumption +(= main_0_temp_i_1 (ite (bvult main_0_i_1 bv13[32]) main_0_i_1 main_0_temp_i_0)) + :extrafuns ((main_0_i_2 BitVec[32])) + :assumption +(= main_0_i_2 (ite (bvult main_0_i_1 bv13[32]) (bvadd main_0_i_1 bv1[32]) main_0_i_1)) + :extrafuns ((main_0_tmp_2 BitVec[32])) + :assumption +(= main_0_tmp_2 (ite (bvult main_0_i_2 bv13[32]) bv2[32] main_0_tmp_1)) + :extrafuns ((arr_val_3 Array[32:32])) + :assumption +(= arr_val_3 (ite (bvult main_0_i_2 bv13[32]) (store arr_val_2 main_0_tmp_2 main_0_i_2) arr_val_2)) + :extrafuns ((arr_next_4 Array[32:32])) + :assumption +(= arr_next_4 (ite (bvult main_0_i_2 bv13[32]) (store arr_next_3 main_0_curr_2 main_0_tmp_2) arr_next_3)) + :extrafuns ((main_0_curr_3 BitVec[32])) + :assumption +(= main_0_curr_3 (ite (bvult main_0_i_2 bv13[32]) (select arr_next_4 main_0_curr_2) main_0_curr_2)) + :extrafuns ((arr_next_5 Array[32:32])) + :assumption +(= arr_next_5 (ite (bvult main_0_i_2 bv13[32]) (store arr_next_4 main_0_tmp_2 (bvneg bv1[32])) arr_next_4)) + :extrafuns ((main_0_temp_i_2 BitVec[32])) + :assumption +(= main_0_temp_i_2 (ite (bvult main_0_i_2 bv13[32]) main_0_i_2 main_0_temp_i_1)) + :extrafuns ((main_0_i_3 BitVec[32])) + :assumption +(= main_0_i_3 (ite (bvult main_0_i_2 bv13[32]) (bvadd main_0_i_2 bv1[32]) main_0_i_2)) + :extrafuns ((main_0_tmp_3 BitVec[32])) + :assumption +(= main_0_tmp_3 (ite (bvult main_0_i_3 bv13[32]) bv3[32] main_0_tmp_2)) + :extrafuns ((arr_val_4 Array[32:32])) + :assumption +(= arr_val_4 (ite (bvult main_0_i_3 bv13[32]) (store arr_val_3 main_0_tmp_3 main_0_i_3) arr_val_3)) + :extrafuns ((arr_next_6 Array[32:32])) + :assumption +(= arr_next_6 (ite (bvult main_0_i_3 bv13[32]) (store arr_next_5 main_0_curr_3 main_0_tmp_3) arr_next_5)) + :extrafuns ((main_0_curr_4 BitVec[32])) + :assumption +(= main_0_curr_4 (ite (bvult main_0_i_3 bv13[32]) (select arr_next_6 main_0_curr_3) main_0_curr_3)) + :extrafuns ((arr_next_7 Array[32:32])) + :assumption +(= arr_next_7 (ite (bvult main_0_i_3 bv13[32]) (store arr_next_6 main_0_tmp_3 (bvneg bv1[32])) arr_next_6)) + :extrafuns ((main_0_temp_i_3 BitVec[32])) + :assumption +(= main_0_temp_i_3 (ite (bvult main_0_i_3 bv13[32]) main_0_i_3 main_0_temp_i_2)) + :extrafuns ((main_0_i_4 BitVec[32])) + :assumption +(= main_0_i_4 (ite (bvult main_0_i_3 bv13[32]) (bvadd main_0_i_3 bv1[32]) main_0_i_3)) + :extrafuns ((main_0_tmp_4 BitVec[32])) + :assumption +(= main_0_tmp_4 (ite (bvult main_0_i_4 bv13[32]) bv4[32] main_0_tmp_3)) + :extrafuns ((arr_val_5 Array[32:32])) + :assumption +(= arr_val_5 (ite (bvult main_0_i_4 bv13[32]) (store arr_val_4 main_0_tmp_4 main_0_i_4) arr_val_4)) + :extrafuns ((arr_next_8 Array[32:32])) + :assumption +(= arr_next_8 (ite (bvult main_0_i_4 bv13[32]) (store arr_next_7 main_0_curr_4 main_0_tmp_4) arr_next_7)) + :extrafuns ((main_0_curr_5 BitVec[32])) + :assumption +(= main_0_curr_5 (ite (bvult main_0_i_4 bv13[32]) (select arr_next_8 main_0_curr_4) main_0_curr_4)) + :extrafuns ((arr_next_9 Array[32:32])) + :assumption +(= arr_next_9 (ite (bvult main_0_i_4 bv13[32]) (store arr_next_8 main_0_tmp_4 (bvneg bv1[32])) arr_next_8)) + :extrafuns ((main_0_temp_i_4 BitVec[32])) + :assumption +(= main_0_temp_i_4 (ite (bvult main_0_i_4 bv13[32]) main_0_i_4 main_0_temp_i_3)) + :extrafuns ((main_0_i_5 BitVec[32])) + :assumption +(= main_0_i_5 (ite (bvult main_0_i_4 bv13[32]) (bvadd main_0_i_4 bv1[32]) main_0_i_4)) + :extrafuns ((main_0_tmp_5 BitVec[32])) + :assumption +(= main_0_tmp_5 (ite (bvult main_0_i_5 bv13[32]) bv5[32] main_0_tmp_4)) + :extrafuns ((arr_val_6 Array[32:32])) + :assumption +(= arr_val_6 (ite (bvult main_0_i_5 bv13[32]) (store arr_val_5 main_0_tmp_5 main_0_i_5) arr_val_5)) + :extrafuns ((arr_next_10 Array[32:32])) + :assumption +(= arr_next_10 (ite (bvult main_0_i_5 bv13[32]) (store arr_next_9 main_0_curr_5 main_0_tmp_5) arr_next_9)) + :extrafuns ((main_0_curr_6 BitVec[32])) + :assumption +(= main_0_curr_6 (ite (bvult main_0_i_5 bv13[32]) (select arr_next_10 main_0_curr_5) main_0_curr_5)) + :extrafuns ((arr_next_11 Array[32:32])) + :assumption +(= arr_next_11 (ite (bvult main_0_i_5 bv13[32]) (store arr_next_10 main_0_tmp_5 (bvneg bv1[32])) arr_next_10)) + :extrafuns ((main_0_temp_i_5 BitVec[32])) + :assumption +(= main_0_temp_i_5 (ite (bvult main_0_i_5 bv13[32]) main_0_i_5 main_0_temp_i_4)) + :extrafuns ((main_0_i_6 BitVec[32])) + :assumption +(= main_0_i_6 (ite (bvult main_0_i_5 bv13[32]) (bvadd main_0_i_5 bv1[32]) main_0_i_5)) + :extrafuns ((main_0_tmp_6 BitVec[32])) + :assumption +(= main_0_tmp_6 (ite (bvult main_0_i_6 bv13[32]) bv6[32] main_0_tmp_5)) + :extrafuns ((arr_val_7 Array[32:32])) + :assumption +(= arr_val_7 (ite (bvult main_0_i_6 bv13[32]) (store arr_val_6 main_0_tmp_6 main_0_i_6) arr_val_6)) + :extrafuns ((arr_next_12 Array[32:32])) + :assumption +(= arr_next_12 (ite (bvult main_0_i_6 bv13[32]) (store arr_next_11 main_0_curr_6 main_0_tmp_6) arr_next_11)) + :extrafuns ((main_0_curr_7 BitVec[32])) + :assumption +(= main_0_curr_7 (ite (bvult main_0_i_6 bv13[32]) (select arr_next_12 main_0_curr_6) main_0_curr_6)) + :extrafuns ((arr_next_13 Array[32:32])) + :assumption +(= arr_next_13 (ite (bvult main_0_i_6 bv13[32]) (store arr_next_12 main_0_tmp_6 (bvneg bv1[32])) arr_next_12)) + :extrafuns ((main_0_temp_i_6 BitVec[32])) + :assumption +(= main_0_temp_i_6 (ite (bvult main_0_i_6 bv13[32]) main_0_i_6 main_0_temp_i_5)) + :extrafuns ((main_0_i_7 BitVec[32])) + :assumption +(= main_0_i_7 (ite (bvult main_0_i_6 bv13[32]) (bvadd main_0_i_6 bv1[32]) main_0_i_6)) + :extrafuns ((main_0_tmp_7 BitVec[32])) + :assumption +(= main_0_tmp_7 (ite (bvult main_0_i_7 bv13[32]) bv7[32] main_0_tmp_6)) + :extrafuns ((arr_val_8 Array[32:32])) + :assumption +(= arr_val_8 (ite (bvult main_0_i_7 bv13[32]) (store arr_val_7 main_0_tmp_7 main_0_i_7) arr_val_7)) + :extrafuns ((arr_next_14 Array[32:32])) + :assumption +(= arr_next_14 (ite (bvult main_0_i_7 bv13[32]) (store arr_next_13 main_0_curr_7 main_0_tmp_7) arr_next_13)) + :extrafuns ((main_0_curr_8 BitVec[32])) + :assumption +(= main_0_curr_8 (ite (bvult main_0_i_7 bv13[32]) (select arr_next_14 main_0_curr_7) main_0_curr_7)) + :extrafuns ((arr_next_15 Array[32:32])) + :assumption +(= arr_next_15 (ite (bvult main_0_i_7 bv13[32]) (store arr_next_14 main_0_tmp_7 (bvneg bv1[32])) arr_next_14)) + :extrafuns ((main_0_temp_i_7 BitVec[32])) + :assumption +(= main_0_temp_i_7 (ite (bvult main_0_i_7 bv13[32]) main_0_i_7 main_0_temp_i_6)) + :extrafuns ((main_0_i_8 BitVec[32])) + :assumption +(= main_0_i_8 (ite (bvult main_0_i_7 bv13[32]) (bvadd main_0_i_7 bv1[32]) main_0_i_7)) + :extrafuns ((main_0_tmp_8 BitVec[32])) + :assumption +(= main_0_tmp_8 (ite (bvult main_0_i_8 bv13[32]) bv8[32] main_0_tmp_7)) + :extrafuns ((arr_val_9 Array[32:32])) + :assumption +(= arr_val_9 (ite (bvult main_0_i_8 bv13[32]) (store arr_val_8 main_0_tmp_8 main_0_i_8) arr_val_8)) + :extrafuns ((arr_next_16 Array[32:32])) + :assumption +(= arr_next_16 (ite (bvult main_0_i_8 bv13[32]) (store arr_next_15 main_0_curr_8 main_0_tmp_8) arr_next_15)) + :extrafuns ((main_0_curr_9 BitVec[32])) + :assumption +(= main_0_curr_9 (ite (bvult main_0_i_8 bv13[32]) (select arr_next_16 main_0_curr_8) main_0_curr_8)) + :extrafuns ((arr_next_17 Array[32:32])) + :assumption +(= arr_next_17 (ite (bvult main_0_i_8 bv13[32]) (store arr_next_16 main_0_tmp_8 (bvneg bv1[32])) arr_next_16)) + :extrafuns ((main_0_temp_i_8 BitVec[32])) + :assumption +(= main_0_temp_i_8 (ite (bvult main_0_i_8 bv13[32]) main_0_i_8 main_0_temp_i_7)) + :extrafuns ((main_0_i_9 BitVec[32])) + :assumption +(= main_0_i_9 (ite (bvult main_0_i_8 bv13[32]) (bvadd main_0_i_8 bv1[32]) main_0_i_8)) + :extrafuns ((main_0_tmp_9 BitVec[32])) + :assumption +(= main_0_tmp_9 (ite (bvult main_0_i_9 bv13[32]) bv9[32] main_0_tmp_8)) + :extrafuns ((arr_val_10 Array[32:32])) + :assumption +(= arr_val_10 (ite (bvult main_0_i_9 bv13[32]) (store arr_val_9 main_0_tmp_9 main_0_i_9) arr_val_9)) + :extrafuns ((arr_next_18 Array[32:32])) + :assumption +(= arr_next_18 (ite (bvult main_0_i_9 bv13[32]) (store arr_next_17 main_0_curr_9 main_0_tmp_9) arr_next_17)) + :extrafuns ((main_0_curr_10 BitVec[32])) + :assumption +(= main_0_curr_10 (ite (bvult main_0_i_9 bv13[32]) (select arr_next_18 main_0_curr_9) main_0_curr_9)) + :extrafuns ((arr_next_19 Array[32:32])) + :assumption +(= arr_next_19 (ite (bvult main_0_i_9 bv13[32]) (store arr_next_18 main_0_tmp_9 (bvneg bv1[32])) arr_next_18)) + :extrafuns ((main_0_temp_i_9 BitVec[32])) + :assumption +(= main_0_temp_i_9 (ite (bvult main_0_i_9 bv13[32]) main_0_i_9 main_0_temp_i_8)) + :extrafuns ((main_0_i_10 BitVec[32])) + :assumption +(= main_0_i_10 (ite (bvult main_0_i_9 bv13[32]) (bvadd main_0_i_9 bv1[32]) main_0_i_9)) + :extrafuns ((main_0_tmp_10 BitVec[32])) + :assumption +(= main_0_tmp_10 (ite (bvult main_0_i_10 bv13[32]) bv10[32] main_0_tmp_9)) + :extrafuns ((arr_val_11 Array[32:32])) + :assumption +(= arr_val_11 (ite (bvult main_0_i_10 bv13[32]) (store arr_val_10 main_0_tmp_10 main_0_i_10) arr_val_10)) + :extrafuns ((arr_next_20 Array[32:32])) + :assumption +(= arr_next_20 (ite (bvult main_0_i_10 bv13[32]) (store arr_next_19 main_0_curr_10 main_0_tmp_10) arr_next_19)) + :extrafuns ((main_0_curr_11 BitVec[32])) + :assumption +(= main_0_curr_11 (ite (bvult main_0_i_10 bv13[32]) (select arr_next_20 main_0_curr_10) main_0_curr_10)) + :extrafuns ((arr_next_21 Array[32:32])) + :assumption +(= arr_next_21 (ite (bvult main_0_i_10 bv13[32]) (store arr_next_20 main_0_tmp_10 (bvneg bv1[32])) arr_next_20)) + :extrafuns ((main_0_temp_i_10 BitVec[32])) + :assumption +(= main_0_temp_i_10 (ite (bvult main_0_i_10 bv13[32]) main_0_i_10 main_0_temp_i_9)) + :extrafuns ((main_0_i_11 BitVec[32])) + :assumption +(= main_0_i_11 (ite (bvult main_0_i_10 bv13[32]) (bvadd main_0_i_10 bv1[32]) main_0_i_10)) + :extrafuns ((main_0_tmp_11 BitVec[32])) + :assumption +(= main_0_tmp_11 (ite (bvult main_0_i_11 bv13[32]) bv11[32] main_0_tmp_10)) + :extrafuns ((arr_val_12 Array[32:32])) + :assumption +(= arr_val_12 (ite (bvult main_0_i_11 bv13[32]) (store arr_val_11 main_0_tmp_11 main_0_i_11) arr_val_11)) + :extrafuns ((arr_next_22 Array[32:32])) + :assumption +(= arr_next_22 (ite (bvult main_0_i_11 bv13[32]) (store arr_next_21 main_0_curr_11 main_0_tmp_11) arr_next_21)) + :extrafuns ((main_0_curr_12 BitVec[32])) + :assumption +(= main_0_curr_12 (ite (bvult main_0_i_11 bv13[32]) (select arr_next_22 main_0_curr_11) main_0_curr_11)) + :extrafuns ((arr_next_23 Array[32:32])) + :assumption +(= arr_next_23 (ite (bvult main_0_i_11 bv13[32]) (store arr_next_22 main_0_tmp_11 (bvneg bv1[32])) arr_next_22)) + :extrafuns ((main_0_temp_i_11 BitVec[32])) + :assumption +(= main_0_temp_i_11 (ite (bvult main_0_i_11 bv13[32]) main_0_i_11 main_0_temp_i_10)) + :extrafuns ((main_0_i_12 BitVec[32])) + :assumption +(= main_0_i_12 (ite (bvult main_0_i_11 bv13[32]) (bvadd main_0_i_11 bv1[32]) main_0_i_11)) + :extrafuns ((main_0_tmp_12 BitVec[32])) + :assumption +(= main_0_tmp_12 (ite (bvult main_0_i_12 bv13[32]) bv12[32] main_0_tmp_11)) + :extrafuns ((arr_val_13 Array[32:32])) + :assumption +(= arr_val_13 (ite (bvult main_0_i_12 bv13[32]) (store arr_val_12 main_0_tmp_12 main_0_i_12) arr_val_12)) + :extrafuns ((arr_next_24 Array[32:32])) + :assumption +(= arr_next_24 (ite (bvult main_0_i_12 bv13[32]) (store arr_next_23 main_0_curr_12 main_0_tmp_12) arr_next_23)) + :extrafuns ((main_0_curr_13 BitVec[32])) + :assumption +(= main_0_curr_13 (ite (bvult main_0_i_12 bv13[32]) (select arr_next_24 main_0_curr_12) main_0_curr_12)) + :extrafuns ((arr_next_25 Array[32:32])) + :assumption +(= arr_next_25 (ite (bvult main_0_i_12 bv13[32]) (store arr_next_24 main_0_tmp_12 (bvneg bv1[32])) arr_next_24)) + :extrafuns ((main_0_temp_i_12 BitVec[32])) + :assumption +(= main_0_temp_i_12 (ite (bvult main_0_i_12 bv13[32]) main_0_i_12 main_0_temp_i_11)) + :extrafuns ((main_0_i_13 BitVec[32])) + :assumption +(= main_0_i_13 (ite (bvult main_0_i_12 bv13[32]) (bvadd main_0_i_12 bv1[32]) main_0_i_12)) + :extrafuns ((main_0_tmp_13 BitVec[32])) + :assumption +(= main_0_tmp_13 (ite (bvult main_0_i_13 bv13[32]) bv13[32] main_0_tmp_12)) + :extrafuns ((arr_val_14 Array[32:32])) + :assumption +(= arr_val_14 (ite (bvult main_0_i_13 bv13[32]) (store arr_val_13 main_0_tmp_13 main_0_i_13) arr_val_13)) + :extrafuns ((arr_next_26 Array[32:32])) + :assumption +(= arr_next_26 (ite (bvult main_0_i_13 bv13[32]) (store arr_next_25 main_0_curr_13 main_0_tmp_13) arr_next_25)) + :extrafuns ((main_0_curr_14 BitVec[32])) + :assumption +(= main_0_curr_14 (ite (bvult main_0_i_13 bv13[32]) (select arr_next_26 main_0_curr_13) main_0_curr_13)) + :extrafuns ((arr_next_27 Array[32:32])) + :assumption +(= arr_next_27 (ite (bvult main_0_i_13 bv13[32]) (store arr_next_26 main_0_tmp_13 (bvneg bv1[32])) arr_next_26)) + :extrafuns ((main_0_temp_i_13 BitVec[32])) + :assumption +(= main_0_temp_i_13 (ite (bvult main_0_i_13 bv13[32]) main_0_i_13 main_0_temp_i_12)) + :extrafuns ((main_0_i_14 BitVec[32])) + :assumption +(= main_0_i_14 (ite (bvult main_0_i_13 bv13[32]) (bvadd main_0_i_13 bv1[32]) main_0_i_13)) + :extrafuns ((main_0_tmp_14 BitVec[32])) + :assumption +(= main_0_tmp_14 (ite (bvult main_0_i_14 bv13[32]) bv14[32] main_0_tmp_13)) + :extrafuns ((arr_val_15 Array[32:32])) + :assumption +(= arr_val_15 (ite (bvult main_0_i_14 bv13[32]) (store arr_val_14 main_0_tmp_14 main_0_i_14) arr_val_14)) + :extrafuns ((arr_next_28 Array[32:32])) + :assumption +(= arr_next_28 (ite (bvult main_0_i_14 bv13[32]) (store arr_next_27 main_0_curr_14 main_0_tmp_14) arr_next_27)) + :extrafuns ((main_0_curr_15 BitVec[32])) + :assumption +(= main_0_curr_15 (ite (bvult main_0_i_14 bv13[32]) (select arr_next_28 main_0_curr_14) main_0_curr_14)) + :extrafuns ((arr_next_29 Array[32:32])) + :assumption +(= arr_next_29 (ite (bvult main_0_i_14 bv13[32]) (store arr_next_28 main_0_tmp_14 (bvneg bv1[32])) arr_next_28)) + :extrafuns ((main_0_temp_i_14 BitVec[32])) + :assumption +(= main_0_temp_i_14 (ite (bvult main_0_i_14 bv13[32]) main_0_i_14 main_0_temp_i_13)) + :extrafuns ((main_0_i_15 BitVec[32])) + :assumption +(= main_0_i_15 (ite (bvult main_0_i_14 bv13[32]) (bvadd main_0_i_14 bv1[32]) main_0_i_14)) + :extrafuns ((undefInt_1 BitVec[32])) + :extrafuns ((delete_0_val_0 BitVec[32])) + :extrafuns ((delete_0_val_1 BitVec[32])) + :assumption +(= delete_0_val_1 undefInt_1) + :extrafuns ((delete_0_list_0 BitVec[32])) + :extrafuns ((delete_0_list_1 BitVec[32])) + :assumption +(= delete_0_list_1 main_0_head_1) + :extrafuns ((delete_0_head_0 BitVec[32])) + :extrafuns ((delete_0_head_1 BitVec[32])) + :assumption +(= delete_0_head_1 delete_0_list_1) + :extrafuns ((delete_0_head_2 BitVec[32])) + :assumption +(let (?cvc_0 (select arr_next_29 delete_0_head_1)) (= delete_0_head_2 (ite (and (= (select arr_val_15 delete_0_head_1) delete_0_val_1) (not (= ?cvc_0 (bvneg bv1[32])))) ?cvc_0 delete_0_head_1))) + :extrafuns ((delete_0_head_3 BitVec[32])) + :assumption +(= delete_0_head_3 (ite (and (= (select arr_val_15 delete_0_head_2) delete_0_val_1) (not (= (select arr_next_29 delete_0_head_1) (bvneg bv1[32])))) (select arr_next_29 delete_0_head_2) delete_0_head_2)) + :extrafuns ((delete_0_head_4 BitVec[32])) + :assumption +(= delete_0_head_4 (ite (and (= (select arr_val_15 delete_0_head_3) delete_0_val_1) (not (= (select arr_next_29 delete_0_head_1) (bvneg bv1[32])))) (select arr_next_29 delete_0_head_3) delete_0_head_3)) + :extrafuns ((delete_0_head_5 BitVec[32])) + :assumption +(= delete_0_head_5 (ite (and (= (select arr_val_15 delete_0_head_4) delete_0_val_1) (not (= (select arr_next_29 delete_0_head_1) (bvneg bv1[32])))) (select arr_next_29 delete_0_head_4) delete_0_head_4)) + :extrafuns ((delete_0_head_6 BitVec[32])) + :assumption +(= delete_0_head_6 (ite (and (= (select arr_val_15 delete_0_head_5) delete_0_val_1) (not (= (select arr_next_29 delete_0_head_1) (bvneg bv1[32])))) (select arr_next_29 delete_0_head_5) delete_0_head_5)) + :extrafuns ((delete_0_head_7 BitVec[32])) + :assumption +(= delete_0_head_7 (ite (and (= (select arr_val_15 delete_0_head_6) delete_0_val_1) (not (= (select arr_next_29 delete_0_head_1) (bvneg bv1[32])))) (select arr_next_29 delete_0_head_6) delete_0_head_6)) + :extrafuns ((delete_0_head_8 BitVec[32])) + :assumption +(= delete_0_head_8 (ite (and (= (select arr_val_15 delete_0_head_7) delete_0_val_1) (not (= (select arr_next_29 delete_0_head_1) (bvneg bv1[32])))) (select arr_next_29 delete_0_head_7) delete_0_head_7)) + :extrafuns ((delete_0_head_9 BitVec[32])) + :assumption +(= delete_0_head_9 (ite (and (= (select arr_val_15 delete_0_head_8) delete_0_val_1) (not (= (select arr_next_29 delete_0_head_1) (bvneg bv1[32])))) (select arr_next_29 delete_0_head_8) delete_0_head_8)) + :extrafuns ((delete_0_head_10 BitVec[32])) + :assumption +(= delete_0_head_10 (ite (and (= (select arr_val_15 delete_0_head_9) delete_0_val_1) (not (= (select arr_next_29 delete_0_head_1) (bvneg bv1[32])))) (select arr_next_29 delete_0_head_9) delete_0_head_9)) + :extrafuns ((delete_0_head_11 BitVec[32])) + :assumption +(= delete_0_head_11 (ite (and (= (select arr_val_15 delete_0_head_10) delete_0_val_1) (not (= (select arr_next_29 delete_0_head_1) (bvneg bv1[32])))) (select arr_next_29 delete_0_head_10) delete_0_head_10)) + :extrafuns ((delete_0_head_12 BitVec[32])) + :assumption +(= delete_0_head_12 (ite (and (= (select arr_val_15 delete_0_head_11) delete_0_val_1) (not (= (select arr_next_29 delete_0_head_1) (bvneg bv1[32])))) (select arr_next_29 delete_0_head_11) delete_0_head_11)) + :extrafuns ((delete_0_head_13 BitVec[32])) + :assumption +(= delete_0_head_13 (ite (and (= (select arr_val_15 delete_0_head_12) delete_0_val_1) (not (= (select arr_next_29 delete_0_head_1) (bvneg bv1[32])))) (select arr_next_29 delete_0_head_12) delete_0_head_12)) + :extrafuns ((delete_0_head_14 BitVec[32])) + :assumption +(= delete_0_head_14 (ite (and (= (select arr_val_15 delete_0_head_13) delete_0_val_1) (not (= (select arr_next_29 delete_0_head_1) (bvneg bv1[32])))) (select arr_next_29 delete_0_head_13) delete_0_head_13)) + :extrafuns ((delete_0_head_15 BitVec[32])) + :assumption +(= delete_0_head_15 (ite (and (= (select arr_val_15 delete_0_head_14) delete_0_val_1) (not (= (select arr_next_29 delete_0_head_1) (bvneg bv1[32])))) (select arr_next_29 delete_0_head_14) delete_0_head_14)) + :extrafuns ((delete_0_prev_0 BitVec[32])) + :extrafuns ((delete_0_prev_1 BitVec[32])) + :assumption +(= delete_0_prev_1 (ite (not (= (select arr_next_29 delete_0_head_1) (bvneg bv1[32]))) delete_0_head_15 delete_0_prev_0)) + :extrafuns ((delete_0_curr_0 BitVec[32])) + :extrafuns ((delete_0_curr_1 BitVec[32])) + :assumption +(= delete_0_curr_1 (ite (not (= (select arr_next_29 delete_0_head_1) (bvneg bv1[32]))) (select arr_next_29 delete_0_head_15) delete_0_curr_0)) + :extrafuns ((arr_next_30 Array[32:32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= arr_next_30 (ite (and (and (not (= delete_0_curr_1 ?cvc_0)) (= (select arr_val_15 delete_0_curr_1) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (store arr_next_29 delete_0_prev_1 (select arr_next_29 delete_0_curr_1)) arr_next_29))) + :extrafuns ((delete_0_curr_2 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_2 (ite (and (and (not (= delete_0_curr_1 ?cvc_0)) (= (select arr_val_15 delete_0_curr_1) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_30 delete_0_curr_1) delete_0_curr_1))) + :extrafuns ((delete_0_prev_2 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_prev_2 (ite (and (and (not (= delete_0_curr_1 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_1) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) delete_0_curr_2 delete_0_prev_1))) + :extrafuns ((delete_0_curr_3 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_3 (ite (and (and (not (= delete_0_curr_1 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_1) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_30 delete_0_curr_2) delete_0_curr_2))) + :extrafuns ((arr_next_31 Array[32:32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= arr_next_31 (ite (and (and (not (= delete_0_curr_3 ?cvc_0)) (= (select arr_val_15 delete_0_curr_3) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (store arr_next_30 delete_0_prev_2 (select arr_next_30 delete_0_curr_3)) arr_next_30))) + :extrafuns ((delete_0_curr_4 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_4 (ite (and (and (not (= delete_0_curr_3 ?cvc_0)) (= (select arr_val_15 delete_0_curr_3) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_31 delete_0_curr_3) delete_0_curr_3))) + :extrafuns ((delete_0_prev_3 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_prev_3 (ite (and (and (not (= delete_0_curr_3 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_3) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) delete_0_curr_4 delete_0_prev_2))) + :extrafuns ((delete_0_curr_5 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_5 (ite (and (and (not (= delete_0_curr_3 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_3) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_31 delete_0_curr_4) delete_0_curr_4))) + :extrafuns ((arr_next_32 Array[32:32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= arr_next_32 (ite (and (and (not (= delete_0_curr_5 ?cvc_0)) (= (select arr_val_15 delete_0_curr_5) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (store arr_next_31 delete_0_prev_3 (select arr_next_31 delete_0_curr_5)) arr_next_31))) + :extrafuns ((delete_0_curr_6 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_6 (ite (and (and (not (= delete_0_curr_5 ?cvc_0)) (= (select arr_val_15 delete_0_curr_5) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_32 delete_0_curr_5) delete_0_curr_5))) + :extrafuns ((delete_0_prev_4 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_prev_4 (ite (and (and (not (= delete_0_curr_5 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_5) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) delete_0_curr_6 delete_0_prev_3))) + :extrafuns ((delete_0_curr_7 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_7 (ite (and (and (not (= delete_0_curr_5 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_5) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_32 delete_0_curr_6) delete_0_curr_6))) + :extrafuns ((arr_next_33 Array[32:32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= arr_next_33 (ite (and (and (not (= delete_0_curr_7 ?cvc_0)) (= (select arr_val_15 delete_0_curr_7) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (store arr_next_32 delete_0_prev_4 (select arr_next_32 delete_0_curr_7)) arr_next_32))) + :extrafuns ((delete_0_curr_8 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_8 (ite (and (and (not (= delete_0_curr_7 ?cvc_0)) (= (select arr_val_15 delete_0_curr_7) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_33 delete_0_curr_7) delete_0_curr_7))) + :extrafuns ((delete_0_prev_5 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_prev_5 (ite (and (and (not (= delete_0_curr_7 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_7) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) delete_0_curr_8 delete_0_prev_4))) + :extrafuns ((delete_0_curr_9 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_9 (ite (and (and (not (= delete_0_curr_7 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_7) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_33 delete_0_curr_8) delete_0_curr_8))) + :extrafuns ((arr_next_34 Array[32:32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= arr_next_34 (ite (and (and (not (= delete_0_curr_9 ?cvc_0)) (= (select arr_val_15 delete_0_curr_9) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (store arr_next_33 delete_0_prev_5 (select arr_next_33 delete_0_curr_9)) arr_next_33))) + :extrafuns ((delete_0_curr_10 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_10 (ite (and (and (not (= delete_0_curr_9 ?cvc_0)) (= (select arr_val_15 delete_0_curr_9) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_34 delete_0_curr_9) delete_0_curr_9))) + :extrafuns ((delete_0_prev_6 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_prev_6 (ite (and (and (not (= delete_0_curr_9 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_9) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) delete_0_curr_10 delete_0_prev_5))) + :extrafuns ((delete_0_curr_11 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_11 (ite (and (and (not (= delete_0_curr_9 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_9) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_34 delete_0_curr_10) delete_0_curr_10))) + :extrafuns ((arr_next_35 Array[32:32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= arr_next_35 (ite (and (and (not (= delete_0_curr_11 ?cvc_0)) (= (select arr_val_15 delete_0_curr_11) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (store arr_next_34 delete_0_prev_6 (select arr_next_34 delete_0_curr_11)) arr_next_34))) + :extrafuns ((delete_0_curr_12 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_12 (ite (and (and (not (= delete_0_curr_11 ?cvc_0)) (= (select arr_val_15 delete_0_curr_11) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_35 delete_0_curr_11) delete_0_curr_11))) + :extrafuns ((delete_0_prev_7 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_prev_7 (ite (and (and (not (= delete_0_curr_11 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_11) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) delete_0_curr_12 delete_0_prev_6))) + :extrafuns ((delete_0_curr_13 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_13 (ite (and (and (not (= delete_0_curr_11 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_11) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_35 delete_0_curr_12) delete_0_curr_12))) + :extrafuns ((arr_next_36 Array[32:32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= arr_next_36 (ite (and (and (not (= delete_0_curr_13 ?cvc_0)) (= (select arr_val_15 delete_0_curr_13) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (store arr_next_35 delete_0_prev_7 (select arr_next_35 delete_0_curr_13)) arr_next_35))) + :extrafuns ((delete_0_curr_14 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_14 (ite (and (and (not (= delete_0_curr_13 ?cvc_0)) (= (select arr_val_15 delete_0_curr_13) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_36 delete_0_curr_13) delete_0_curr_13))) + :extrafuns ((delete_0_prev_8 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_prev_8 (ite (and (and (not (= delete_0_curr_13 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_13) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) delete_0_curr_14 delete_0_prev_7))) + :extrafuns ((delete_0_curr_15 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_15 (ite (and (and (not (= delete_0_curr_13 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_13) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_36 delete_0_curr_14) delete_0_curr_14))) + :extrafuns ((arr_next_37 Array[32:32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= arr_next_37 (ite (and (and (not (= delete_0_curr_15 ?cvc_0)) (= (select arr_val_15 delete_0_curr_15) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (store arr_next_36 delete_0_prev_8 (select arr_next_36 delete_0_curr_15)) arr_next_36))) + :extrafuns ((delete_0_curr_16 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_16 (ite (and (and (not (= delete_0_curr_15 ?cvc_0)) (= (select arr_val_15 delete_0_curr_15) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_37 delete_0_curr_15) delete_0_curr_15))) + :extrafuns ((delete_0_prev_9 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_prev_9 (ite (and (and (not (= delete_0_curr_15 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_15) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) delete_0_curr_16 delete_0_prev_8))) + :extrafuns ((delete_0_curr_17 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_17 (ite (and (and (not (= delete_0_curr_15 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_15) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_37 delete_0_curr_16) delete_0_curr_16))) + :extrafuns ((arr_next_38 Array[32:32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= arr_next_38 (ite (and (and (not (= delete_0_curr_17 ?cvc_0)) (= (select arr_val_15 delete_0_curr_17) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (store arr_next_37 delete_0_prev_9 (select arr_next_37 delete_0_curr_17)) arr_next_37))) + :extrafuns ((delete_0_curr_18 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_18 (ite (and (and (not (= delete_0_curr_17 ?cvc_0)) (= (select arr_val_15 delete_0_curr_17) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_38 delete_0_curr_17) delete_0_curr_17))) + :extrafuns ((delete_0_prev_10 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_prev_10 (ite (and (and (not (= delete_0_curr_17 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_17) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) delete_0_curr_18 delete_0_prev_9))) + :extrafuns ((delete_0_curr_19 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_19 (ite (and (and (not (= delete_0_curr_17 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_17) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_38 delete_0_curr_18) delete_0_curr_18))) + :extrafuns ((arr_next_39 Array[32:32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= arr_next_39 (ite (and (and (not (= delete_0_curr_19 ?cvc_0)) (= (select arr_val_15 delete_0_curr_19) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (store arr_next_38 delete_0_prev_10 (select arr_next_38 delete_0_curr_19)) arr_next_38))) + :extrafuns ((delete_0_curr_20 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_20 (ite (and (and (not (= delete_0_curr_19 ?cvc_0)) (= (select arr_val_15 delete_0_curr_19) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_39 delete_0_curr_19) delete_0_curr_19))) + :extrafuns ((delete_0_prev_11 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_prev_11 (ite (and (and (not (= delete_0_curr_19 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_19) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) delete_0_curr_20 delete_0_prev_10))) + :extrafuns ((delete_0_curr_21 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_21 (ite (and (and (not (= delete_0_curr_19 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_19) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_39 delete_0_curr_20) delete_0_curr_20))) + :extrafuns ((arr_next_40 Array[32:32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= arr_next_40 (ite (and (and (not (= delete_0_curr_21 ?cvc_0)) (= (select arr_val_15 delete_0_curr_21) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (store arr_next_39 delete_0_prev_11 (select arr_next_39 delete_0_curr_21)) arr_next_39))) + :extrafuns ((delete_0_curr_22 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_22 (ite (and (and (not (= delete_0_curr_21 ?cvc_0)) (= (select arr_val_15 delete_0_curr_21) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_40 delete_0_curr_21) delete_0_curr_21))) + :extrafuns ((delete_0_prev_12 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_prev_12 (ite (and (and (not (= delete_0_curr_21 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_21) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) delete_0_curr_22 delete_0_prev_11))) + :extrafuns ((delete_0_curr_23 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_23 (ite (and (and (not (= delete_0_curr_21 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_21) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_40 delete_0_curr_22) delete_0_curr_22))) + :extrafuns ((arr_next_41 Array[32:32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= arr_next_41 (ite (and (and (not (= delete_0_curr_23 ?cvc_0)) (= (select arr_val_15 delete_0_curr_23) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (store arr_next_40 delete_0_prev_12 (select arr_next_40 delete_0_curr_23)) arr_next_40))) + :extrafuns ((delete_0_curr_24 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_24 (ite (and (and (not (= delete_0_curr_23 ?cvc_0)) (= (select arr_val_15 delete_0_curr_23) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_41 delete_0_curr_23) delete_0_curr_23))) + :extrafuns ((delete_0_prev_13 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_prev_13 (ite (and (and (not (= delete_0_curr_23 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_23) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) delete_0_curr_24 delete_0_prev_12))) + :extrafuns ((delete_0_curr_25 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_25 (ite (and (and (not (= delete_0_curr_23 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_23) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_41 delete_0_curr_24) delete_0_curr_24))) + :extrafuns ((arr_next_42 Array[32:32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= arr_next_42 (ite (and (and (not (= delete_0_curr_25 ?cvc_0)) (= (select arr_val_15 delete_0_curr_25) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (store arr_next_41 delete_0_prev_13 (select arr_next_41 delete_0_curr_25)) arr_next_41))) + :extrafuns ((delete_0_curr_26 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_26 (ite (and (and (not (= delete_0_curr_25 ?cvc_0)) (= (select arr_val_15 delete_0_curr_25) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_42 delete_0_curr_25) delete_0_curr_25))) + :extrafuns ((delete_0_prev_14 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_prev_14 (ite (and (and (not (= delete_0_curr_25 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_25) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) delete_0_curr_26 delete_0_prev_13))) + :extrafuns ((delete_0_curr_27 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_27 (ite (and (and (not (= delete_0_curr_25 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_25) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_42 delete_0_curr_26) delete_0_curr_26))) + :extrafuns ((arr_next_43 Array[32:32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= arr_next_43 (ite (and (and (not (= delete_0_curr_27 ?cvc_0)) (= (select arr_val_15 delete_0_curr_27) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (store arr_next_42 delete_0_prev_14 (select arr_next_42 delete_0_curr_27)) arr_next_42))) + :extrafuns ((delete_0_curr_28 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_28 (ite (and (and (not (= delete_0_curr_27 ?cvc_0)) (= (select arr_val_15 delete_0_curr_27) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_43 delete_0_curr_27) delete_0_curr_27))) + :extrafuns ((delete_0_prev_15 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_prev_15 (ite (and (and (not (= delete_0_curr_27 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_27) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) delete_0_curr_28 delete_0_prev_14))) + :extrafuns ((delete_0_curr_29 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_29 (ite (and (and (not (= delete_0_curr_27 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_27) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_43 delete_0_curr_28) delete_0_curr_28))) + :extrafuns ((delete_return_0 BitVec[32])) + :extrafuns ((delete_return_1 BitVec[32])) + :assumption +(= delete_return_1 delete_0_head_15) + :extrafuns ((main_0_head_2 BitVec[32])) + :assumption +(= main_0_head_2 delete_return_1) + :extrafuns ((main_0_x_0 BitVec[32])) + :extrafuns ((member_0_val_0 BitVec[32])) + :extrafuns ((member_0_val_1 BitVec[32])) + :assumption +(= member_0_val_1 bv0[32]) + :extrafuns ((member_0_head_0 BitVec[32])) + :extrafuns ((member_0_head_1 BitVec[32])) + :assumption +(= member_0_head_1 main_0_head_2) + :extrafuns ((member_0_curr_0 BitVec[32])) + :extrafuns ((member_0_curr_1 BitVec[32])) + :assumption +(= member_0_curr_1 member_0_head_1) + :extrafuns ((member_0_result_0 BitVec[32])) + :extrafuns ((member_0_result_1 BitVec[32])) + :assumption +(= member_0_result_1 (ite (and (not (= member_0_curr_1 (bvneg bv1[32]))) (= (select arr_val_15 member_0_curr_1) member_0_val_1)) bv1[32] member_0_result_0)) + :extrafuns ((member_0_curr_2 BitVec[32])) + :assumption +(flet ($cvc_0 (not (= member_0_curr_1 (bvneg bv1[32])))) (= member_0_curr_2 (ite (and (not (and $cvc_0 (= (select arr_val_15 member_0_curr_1) member_0_val_1))) $cvc_0) (select arr_next_43 member_0_curr_1) member_0_curr_1))) + :extrafuns ((member_0_result_2 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= member_0_result_2 (ite (and (and (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1))) (not (= member_0_curr_2 ?cvc_0))) (= (select arr_val_15 member_0_curr_2) member_0_val_1)) bv1[32] member_0_result_1))) + :extrafuns ((member_0_curr_3 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (flet ($cvc_1 (not (= member_0_curr_2 ?cvc_0))) (= member_0_curr_3 (ite (and (and (not (and $cvc_1 (= (select arr_val_15 member_0_curr_2) member_0_val_1))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) $cvc_1) (select arr_next_43 member_0_curr_2) member_0_curr_2)))) + :extrafuns ((member_0_result_3 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= member_0_result_3 (ite (and (and (and (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) (not (= member_0_curr_3 ?cvc_0))) (= (select arr_val_15 member_0_curr_3) member_0_val_1)) bv1[32] member_0_result_2))) + :extrafuns ((member_0_curr_4 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (flet ($cvc_1 (not (= member_0_curr_3 ?cvc_0))) (= member_0_curr_4 (ite (and (and (and (not (and $cvc_1 (= (select arr_val_15 member_0_curr_3) member_0_val_1))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) $cvc_1) (select arr_next_43 member_0_curr_3) member_0_curr_3)))) + :extrafuns ((member_0_result_4 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= member_0_result_4 (ite (and (and (and (and (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) (not (= member_0_curr_4 ?cvc_0))) (= (select arr_val_15 member_0_curr_4) member_0_val_1)) bv1[32] member_0_result_3))) + :extrafuns ((member_0_curr_5 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (flet ($cvc_1 (not (= member_0_curr_4 ?cvc_0))) (= member_0_curr_5 (ite (and (and (and (and (not (and $cvc_1 (= (select arr_val_15 member_0_curr_4) member_0_val_1))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) $cvc_1) (select arr_next_43 member_0_curr_4) member_0_curr_4)))) + :extrafuns ((member_0_result_5 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= member_0_result_5 (ite (and (and (and (and (and (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) (not (= member_0_curr_5 ?cvc_0))) (= (select arr_val_15 member_0_curr_5) member_0_val_1)) bv1[32] member_0_result_4))) + :extrafuns ((member_0_curr_6 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (flet ($cvc_1 (not (= member_0_curr_5 ?cvc_0))) (= member_0_curr_6 (ite (and (and (and (and (and (not (and $cvc_1 (= (select arr_val_15 member_0_curr_5) member_0_val_1))) (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) $cvc_1) (select arr_next_43 member_0_curr_5) member_0_curr_5)))) + :extrafuns ((member_0_result_6 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= member_0_result_6 (ite (and (and (and (and (and (and (not (and (not (= member_0_curr_5 ?cvc_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1))) (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) (not (= member_0_curr_6 ?cvc_0))) (= (select arr_val_15 member_0_curr_6) member_0_val_1)) bv1[32] member_0_result_5))) + :extrafuns ((member_0_curr_7 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (flet ($cvc_1 (not (= member_0_curr_6 ?cvc_0))) (= member_0_curr_7 (ite (and (and (and (and (and (and (not (and $cvc_1 (= (select arr_val_15 member_0_curr_6) member_0_val_1))) (not (and (not (= member_0_curr_5 ?cvc_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) $cvc_1) (select arr_next_43 member_0_curr_6) member_0_curr_6)))) + :extrafuns ((member_0_result_7 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= member_0_result_7 (ite (and (and (and (and (and (and (and (not (and (not (= member_0_curr_6 ?cvc_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1))) (not (and (not (= member_0_curr_5 ?cvc_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) (not (= member_0_curr_7 ?cvc_0))) (= (select arr_val_15 member_0_curr_7) member_0_val_1)) bv1[32] member_0_result_6))) + :extrafuns ((member_0_curr_8 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (flet ($cvc_1 (not (= member_0_curr_7 ?cvc_0))) (= member_0_curr_8 (ite (and (and (and (and (and (and (and (not (and $cvc_1 (= (select arr_val_15 member_0_curr_7) member_0_val_1))) (not (and (not (= member_0_curr_6 ?cvc_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 ?cvc_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) $cvc_1) (select arr_next_43 member_0_curr_7) member_0_curr_7)))) + :extrafuns ((member_0_result_8 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= member_0_result_8 (ite (and (and (and (and (and (and (and (and (not (and (not (= member_0_curr_7 ?cvc_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1))) (not (and (not (= member_0_curr_6 ?cvc_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 ?cvc_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) (not (= member_0_curr_8 ?cvc_0))) (= (select arr_val_15 member_0_curr_8) member_0_val_1)) bv1[32] member_0_result_7))) + :extrafuns ((member_0_curr_9 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (flet ($cvc_1 (not (= member_0_curr_8 ?cvc_0))) (= member_0_curr_9 (ite (and (and (and (and (and (and (and (and (not (and $cvc_1 (= (select arr_val_15 member_0_curr_8) member_0_val_1))) (not (and (not (= member_0_curr_7 ?cvc_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1)))) (not (and (not (= member_0_curr_6 ?cvc_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 ?cvc_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) $cvc_1) (select arr_next_43 member_0_curr_8) member_0_curr_8)))) + :extrafuns ((member_0_result_9 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= member_0_result_9 (ite (and (and (and (and (and (and (and (and (and (not (and (not (= member_0_curr_8 ?cvc_0)) (= (select arr_val_15 member_0_curr_8) member_0_val_1))) (not (and (not (= member_0_curr_7 ?cvc_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1)))) (not (and (not (= member_0_curr_6 ?cvc_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 ?cvc_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) (not (= member_0_curr_9 ?cvc_0))) (= (select arr_val_15 member_0_curr_9) member_0_val_1)) bv1[32] member_0_result_8))) + :extrafuns ((member_0_curr_10 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (flet ($cvc_1 (not (= member_0_curr_9 ?cvc_0))) (= member_0_curr_10 (ite (and (and (and (and (and (and (and (and (and (not (and $cvc_1 (= (select arr_val_15 member_0_curr_9) member_0_val_1))) (not (and (not (= member_0_curr_8 ?cvc_0)) (= (select arr_val_15 member_0_curr_8) member_0_val_1)))) (not (and (not (= member_0_curr_7 ?cvc_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1)))) (not (and (not (= member_0_curr_6 ?cvc_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 ?cvc_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) $cvc_1) (select arr_next_43 member_0_curr_9) member_0_curr_9)))) + :extrafuns ((member_0_result_10 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= member_0_result_10 (ite (and (and (and (and (and (and (and (and (and (and (not (and (not (= member_0_curr_9 ?cvc_0)) (= (select arr_val_15 member_0_curr_9) member_0_val_1))) (not (and (not (= member_0_curr_8 ?cvc_0)) (= (select arr_val_15 member_0_curr_8) member_0_val_1)))) (not (and (not (= member_0_curr_7 ?cvc_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1)))) (not (and (not (= member_0_curr_6 ?cvc_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 ?cvc_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) (not (= member_0_curr_10 ?cvc_0))) (= (select arr_val_15 member_0_curr_10) member_0_val_1)) bv1[32] member_0_result_9))) + :extrafuns ((member_0_curr_11 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (flet ($cvc_1 (not (= member_0_curr_10 ?cvc_0))) (= member_0_curr_11 (ite (and (and (and (and (and (and (and (and (and (and (not (and $cvc_1 (= (select arr_val_15 member_0_curr_10) member_0_val_1))) (not (and (not (= member_0_curr_9 ?cvc_0)) (= (select arr_val_15 member_0_curr_9) member_0_val_1)))) (not (and (not (= member_0_curr_8 ?cvc_0)) (= (select arr_val_15 member_0_curr_8) member_0_val_1)))) (not (and (not (= member_0_curr_7 ?cvc_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1)))) (not (and (not (= member_0_curr_6 ?cvc_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 ?cvc_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) $cvc_1) (select arr_next_43 member_0_curr_10) member_0_curr_10)))) + :extrafuns ((member_0_result_11 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= member_0_result_11 (ite (and (and (and (and (and (and (and (and (and (and (and (not (and (not (= member_0_curr_10 ?cvc_0)) (= (select arr_val_15 member_0_curr_10) member_0_val_1))) (not (and (not (= member_0_curr_9 ?cvc_0)) (= (select arr_val_15 member_0_curr_9) member_0_val_1)))) (not (and (not (= member_0_curr_8 ?cvc_0)) (= (select arr_val_15 member_0_curr_8) member_0_val_1)))) (not (and (not (= member_0_curr_7 ?cvc_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1)))) (not (and (not (= member_0_curr_6 ?cvc_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 ?cvc_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) (not (= member_0_curr_11 ?cvc_0))) (= (select arr_val_15 member_0_curr_11) member_0_val_1)) bv1[32] member_0_result_10))) + :extrafuns ((member_0_curr_12 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (flet ($cvc_1 (not (= member_0_curr_11 ?cvc_0))) (= member_0_curr_12 (ite (and (and (and (and (and (and (and (and (and (and (and (not (and $cvc_1 (= (select arr_val_15 member_0_curr_11) member_0_val_1))) (not (and (not (= member_0_curr_10 ?cvc_0)) (= (select arr_val_15 member_0_curr_10) member_0_val_1)))) (not (and (not (= member_0_curr_9 ?cvc_0)) (= (select arr_val_15 member_0_curr_9) member_0_val_1)))) (not (and (not (= member_0_curr_8 ?cvc_0)) (= (select arr_val_15 member_0_curr_8) member_0_val_1)))) (not (and (not (= member_0_curr_7 ?cvc_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1)))) (not (and (not (= member_0_curr_6 ?cvc_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 ?cvc_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) $cvc_1) (select arr_next_43 member_0_curr_11) member_0_curr_11)))) + :extrafuns ((member_0_result_12 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= member_0_result_12 (ite (and (and (and (and (and (and (and (and (and (and (and (and (not (and (not (= member_0_curr_11 ?cvc_0)) (= (select arr_val_15 member_0_curr_11) member_0_val_1))) (not (and (not (= member_0_curr_10 ?cvc_0)) (= (select arr_val_15 member_0_curr_10) member_0_val_1)))) (not (and (not (= member_0_curr_9 ?cvc_0)) (= (select arr_val_15 member_0_curr_9) member_0_val_1)))) (not (and (not (= member_0_curr_8 ?cvc_0)) (= (select arr_val_15 member_0_curr_8) member_0_val_1)))) (not (and (not (= member_0_curr_7 ?cvc_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1)))) (not (and (not (= member_0_curr_6 ?cvc_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 ?cvc_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) (not (= member_0_curr_12 ?cvc_0))) (= (select arr_val_15 member_0_curr_12) member_0_val_1)) bv1[32] member_0_result_11))) + :extrafuns ((member_0_curr_13 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (flet ($cvc_1 (not (= member_0_curr_12 ?cvc_0))) (= member_0_curr_13 (ite (and (and (and (and (and (and (and (and (and (and (and (and (not (and $cvc_1 (= (select arr_val_15 member_0_curr_12) member_0_val_1))) (not (and (not (= member_0_curr_11 ?cvc_0)) (= (select arr_val_15 member_0_curr_11) member_0_val_1)))) (not (and (not (= member_0_curr_10 ?cvc_0)) (= (select arr_val_15 member_0_curr_10) member_0_val_1)))) (not (and (not (= member_0_curr_9 ?cvc_0)) (= (select arr_val_15 member_0_curr_9) member_0_val_1)))) (not (and (not (= member_0_curr_8 ?cvc_0)) (= (select arr_val_15 member_0_curr_8) member_0_val_1)))) (not (and (not (= member_0_curr_7 ?cvc_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1)))) (not (and (not (= member_0_curr_6 ?cvc_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 ?cvc_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) $cvc_1) (select arr_next_43 member_0_curr_12) member_0_curr_12)))) + :extrafuns ((member_0_result_13 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= member_0_result_13 (ite (and (and (and (and (and (and (and (and (and (and (and (and (and (not (and (not (= member_0_curr_12 ?cvc_0)) (= (select arr_val_15 member_0_curr_12) member_0_val_1))) (not (and (not (= member_0_curr_11 ?cvc_0)) (= (select arr_val_15 member_0_curr_11) member_0_val_1)))) (not (and (not (= member_0_curr_10 ?cvc_0)) (= (select arr_val_15 member_0_curr_10) member_0_val_1)))) (not (and (not (= member_0_curr_9 ?cvc_0)) (= (select arr_val_15 member_0_curr_9) member_0_val_1)))) (not (and (not (= member_0_curr_8 ?cvc_0)) (= (select arr_val_15 member_0_curr_8) member_0_val_1)))) (not (and (not (= member_0_curr_7 ?cvc_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1)))) (not (and (not (= member_0_curr_6 ?cvc_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 ?cvc_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) (not (= member_0_curr_13 ?cvc_0))) (= (select arr_val_15 member_0_curr_13) member_0_val_1)) bv1[32] member_0_result_12))) + :extrafuns ((member_0_curr_14 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (flet ($cvc_1 (not (= member_0_curr_13 ?cvc_0))) (= member_0_curr_14 (ite (and (and (and (and (and (and (and (and (and (and (and (and (and (not (and $cvc_1 (= (select arr_val_15 member_0_curr_13) member_0_val_1))) (not (and (not (= member_0_curr_12 ?cvc_0)) (= (select arr_val_15 member_0_curr_12) member_0_val_1)))) (not (and (not (= member_0_curr_11 ?cvc_0)) (= (select arr_val_15 member_0_curr_11) member_0_val_1)))) (not (and (not (= member_0_curr_10 ?cvc_0)) (= (select arr_val_15 member_0_curr_10) member_0_val_1)))) (not (and (not (= member_0_curr_9 ?cvc_0)) (= (select arr_val_15 member_0_curr_9) member_0_val_1)))) (not (and (not (= member_0_curr_8 ?cvc_0)) (= (select arr_val_15 member_0_curr_8) member_0_val_1)))) (not (and (not (= member_0_curr_7 ?cvc_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1)))) (not (and (not (= member_0_curr_6 ?cvc_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 ?cvc_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) $cvc_1) (select arr_next_43 member_0_curr_13) member_0_curr_13)))) + :extrafuns ((member_0_result_14 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= member_0_result_14 (ite (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (and (not (= member_0_curr_13 ?cvc_0)) (= (select arr_val_15 member_0_curr_13) member_0_val_1))) (not (and (not (= member_0_curr_12 ?cvc_0)) (= (select arr_val_15 member_0_curr_12) member_0_val_1)))) (not (and (not (= member_0_curr_11 ?cvc_0)) (= (select arr_val_15 member_0_curr_11) member_0_val_1)))) (not (and (not (= member_0_curr_10 ?cvc_0)) (= (select arr_val_15 member_0_curr_10) member_0_val_1)))) (not (and (not (= member_0_curr_9 ?cvc_0)) (= (select arr_val_15 member_0_curr_9) member_0_val_1)))) (not (and (not (= member_0_curr_8 ?cvc_0)) (= (select arr_val_15 member_0_curr_8) member_0_val_1)))) (not (and (not (= member_0_curr_7 ?cvc_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1)))) (not (and (not (= member_0_curr_6 ?cvc_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 ?cvc_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) (not (= member_0_curr_14 ?cvc_0))) (= (select arr_val_15 member_0_curr_14) member_0_val_1)) bv1[32] member_0_result_13))) + :extrafuns ((member_0_curr_15 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (flet ($cvc_1 (not (= member_0_curr_14 ?cvc_0))) (= member_0_curr_15 (ite (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (and $cvc_1 (= (select arr_val_15 member_0_curr_14) member_0_val_1))) (not (and (not (= member_0_curr_13 ?cvc_0)) (= (select arr_val_15 member_0_curr_13) member_0_val_1)))) (not (and (not (= member_0_curr_12 ?cvc_0)) (= (select arr_val_15 member_0_curr_12) member_0_val_1)))) (not (and (not (= member_0_curr_11 ?cvc_0)) (= (select arr_val_15 member_0_curr_11) member_0_val_1)))) (not (and (not (= member_0_curr_10 ?cvc_0)) (= (select arr_val_15 member_0_curr_10) member_0_val_1)))) (not (and (not (= member_0_curr_9 ?cvc_0)) (= (select arr_val_15 member_0_curr_9) member_0_val_1)))) (not (and (not (= member_0_curr_8 ?cvc_0)) (= (select arr_val_15 member_0_curr_8) member_0_val_1)))) (not (and (not (= member_0_curr_7 ?cvc_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1)))) (not (and (not (= member_0_curr_6 ?cvc_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 ?cvc_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) $cvc_1) (select arr_next_43 member_0_curr_14) member_0_curr_14)))) + :extrafuns ((member_0_result_15 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= member_0_result_15 (ite (and (and (and (and (and (and (and (and (and (and (and (and (and (not (and (not (= member_0_curr_14 ?cvc_0)) (= (select arr_val_15 member_0_curr_14) member_0_val_1))) (not (and (not (= member_0_curr_13 ?cvc_0)) (= (select arr_val_15 member_0_curr_13) member_0_val_1)))) (not (and (not (= member_0_curr_12 ?cvc_0)) (= (select arr_val_15 member_0_curr_12) member_0_val_1)))) (not (and (not (= member_0_curr_11 ?cvc_0)) (= (select arr_val_15 member_0_curr_11) member_0_val_1)))) (not (and (not (= member_0_curr_10 ?cvc_0)) (= (select arr_val_15 member_0_curr_10) member_0_val_1)))) (not (and (not (= member_0_curr_9 ?cvc_0)) (= (select arr_val_15 member_0_curr_9) member_0_val_1)))) (not (and (not (= member_0_curr_8 ?cvc_0)) (= (select arr_val_15 member_0_curr_8) member_0_val_1)))) (not (and (not (= member_0_curr_7 ?cvc_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1)))) (not (and (not (= member_0_curr_6 ?cvc_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 ?cvc_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) bv0[32] member_0_result_14))) + :extrafuns ((main_0_x_1 BitVec[32])) + :assumption +(= main_0_x_1 member_0_result_15) + :formula +(let (?cvc_0 (bvneg bv1[32])) (flet ($cvc_1 (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (flet ($cvc_2 (not (= member_0_curr_14 ?cvc_0))) (not (and (and (and (and (implies (bvult main_0_i_14 bv13[32]) (not (bvult main_0_i_15 bv13[32]))) (implies (and (= (select arr_val_15 delete_0_head_14) delete_0_val_1) $cvc_1) (not (= (select arr_val_15 delete_0_head_15) delete_0_val_1)))) (implies (and (not (= delete_0_curr_27 ?cvc_0)) $cvc_1) (not (not (= delete_0_curr_29 ?cvc_0))))) (implies (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (and $cvc_2 (= (select arr_val_15 member_0_curr_14) member_0_val_1))) (not (and (not (= member_0_curr_13 ?cvc_0)) (= (select arr_val_15 member_0_curr_13) member_0_val_1)))) (not (and (not (= member_0_curr_12 ?cvc_0)) (= (select arr_val_15 member_0_curr_12) member_0_val_1)))) (not (and (not (= member_0_curr_11 ?cvc_0)) (= (select arr_val_15 member_0_curr_11) member_0_val_1)))) (not (and (not (= member_0_curr_10 ?cvc_0)) (= (select arr_val_15 member_0_curr_10) member_0_val_1)))) (not (and (not (= member_0_curr_9 ?cvc_0)) (= (select arr_val_15 member_0_curr_9) member_0_val_1)))) (not (and (not (= member_0_curr_8 ?cvc_0)) (= (select arr_val_15 member_0_curr_8) member_0_val_1)))) (not (and (not (= member_0_curr_7 ?cvc_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1)))) (not (and (not (= member_0_curr_6 ?cvc_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 ?cvc_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) $cvc_2) (not (not (= member_0_curr_15 ?cvc_0))))) (= main_0_x_1 bv0[32])))))) +) diff --git a/test/regress/regress0/aufbv/try5_small_difret_functions_wp_su.set_char_quoting.il.wp.delta01.smt b/test/regress/regress0/aufbv/try5_small_difret_functions_wp_su.set_char_quoting.il.wp.delta01.smt new file mode 100644 index 000000000..028427acc --- /dev/null +++ b/test/regress/regress0/aufbv/try5_small_difret_functions_wp_su.set_char_quoting.il.wp.delta01.smt @@ -0,0 +1,28 @@ +(benchmark B_ +:logic QF_AUFBV +:extrafuns ((R_ESP_1_58 BitVec[32])) +:extrafuns ((mem_35_197 Array[32:8])) +:status sat +:formula +(let (?n1 bv0[32]) +(let (?n2 bv0[24]) +(let (?n3 bv1[32]) +(let (?n4 (bvadd ?n3 R_ESP_1_58)) +(let (?n5 bv0[8]) +(let (?n6 (store mem_35_197 ?n4 ?n5)) +(let (?n7 (bvadd ?n3 ?n4)) +(let (?n8 (store ?n6 ?n7 ?n5)) +(let (?n9 (store ?n8 ?n1 ?n5)) +(let (?n10 (select ?n6 R_ESP_1_58)) +(let (?n11 (concat ?n2 ?n10)) +(let (?n12 (bvadd ?n3 ?n11)) +(let (?n13 (select ?n9 ?n12)) +(let (?n14 (concat ?n2 ?n13)) +(let (?n15 (bvxor ?n3 ?n14)) +(let (?n16 (extract[7:0] ?n15)) +(let (?n17 (store ?n9 ?n12 ?n16)) +(let (?n18 (select ?n17 ?n1)) +(let (?n19 (concat ?n2 ?n18)) +(flet ($n20 (= ?n1 ?n19)) +$n20 +))))))))))))))))))))) diff --git a/test/regress/regress0/aufbv/wchains010ue.delta01.smt b/test/regress/regress0/aufbv/wchains010ue.delta01.smt new file mode 100644 index 000000000..28a892e8d --- /dev/null +++ b/test/regress/regress0/aufbv/wchains010ue.delta01.smt @@ -0,0 +1,36 @@ +(benchmark wchains010ue.smt +:logic QF_AUFBV +:extrafuns ((v6 BitVec[32])) +:extrafuns ((a1 Array[32:8])) +:extrafuns ((v15 BitVec[32])) +:status sat +:formula +(let (?n1 bv0[1]) +(let (?n2 (extract[1:0] v6)) +(let (?n3 bv0[2]) +(flet ($n4 (= ?n2 ?n3)) +(let (?n5 bv1[1]) +(let (?n6 (ite $n4 ?n5 ?n1)) +(let (?n7 bv0[8]) +(let (?n8 (store a1 v15 ?n7)) +(let (?n9 bv1[32]) +(let (?n10 (bvadd ?n9 v15)) +(let (?n11 (store ?n8 ?n10 ?n7)) +(let (?n12 bv3[32]) +(let (?n13 (bvadd ?n12 v15)) +(let (?n14 (store ?n11 ?n13 ?n7)) +(let (?n15 (extract[7:0] v6)) +(let (?n16 (store a1 v6 ?n15)) +(let (?n17 (bvadd ?n9 v6)) +(let (?n18 bv1[8]) +(let (?n19 (store ?n16 ?n17 ?n18)) +(let (?n20 (bvadd ?n12 v6)) +(let (?n21 (store ?n19 ?n20 ?n18)) +(flet ($n22 (= ?n14 ?n21)) +(let (?n23 (ite $n22 ?n5 ?n1)) +(let (?n24 (bvnot ?n23)) +(let (?n25 (bvand ?n6 ?n24)) +(flet ($n26 (= ?n1 ?n25)) +(flet ($n27 (not $n26)) +$n27 +)))))))))))))))))))))))))))) diff --git a/test/regress/regress0/aufbv/wchains010ue.delta02.smt b/test/regress/regress0/aufbv/wchains010ue.delta02.smt new file mode 100644 index 000000000..d5ddf6446 --- /dev/null +++ b/test/regress/regress0/aufbv/wchains010ue.delta02.smt @@ -0,0 +1,35 @@ +(benchmark wchains010ue.smt +:logic QF_AUFBV +:extrafuns ((v6 BitVec[32])) +:extrafuns ((v7 BitVec[32])) +:extrafuns ((a1 Array[32:8])) +:status unsat +:formula +(let (?n1 bv0[1]) +(let (?n2 bv0[2]) +(let (?n3 (extract[1:0] v6)) +(flet ($n4 (= ?n2 ?n3)) +(let (?n5 bv1[1]) +(let (?n6 (ite $n4 ?n5 ?n1)) +(let (?n7 (extract[23:16] v6)) +(let (?n8 (store a1 v6 ?n7)) +(let (?n9 bv0[32]) +(let (?n10 bv0[8]) +(let (?n11 (store ?n8 ?n9 ?n10)) +(let (?n12 (extract[23:16] v7)) +(let (?n13 (store ?n11 v7 ?n12)) +(let (?n14 bv1[32]) +(let (?n15 (store ?n13 ?n14 ?n10)) +(let (?n16 (store ?n15 ?n9 ?n10)) +(let (?n17 (store a1 ?n9 ?n10)) +(let (?n18 (store ?n17 v7 ?n12)) +(let (?n19 (store ?n18 ?n14 ?n10)) +(let (?n20 (store ?n19 v6 ?n7)) +(flet ($n21 (= ?n16 ?n20)) +(let (?n22 (ite $n21 ?n5 ?n1)) +(let (?n23 (bvnot ?n22)) +(let (?n24 (bvand ?n6 ?n23)) +(flet ($n25 (= ?n1 ?n24)) +(flet ($n26 (not $n25)) +$n26 +))))))))))))))))))))))))))) diff --git a/test/regress/regress0/aufbv/wchains010ue.smt b/test/regress/regress0/aufbv/wchains010ue.smt new file mode 100644 index 000000000..a4d0f1ddb --- /dev/null +++ b/test/regress/regress0/aufbv/wchains010ue.smt @@ -0,0 +1,221 @@ +(benchmark wchains010ue.smt +:source { +This benchmark generates write chain permutations and tries to show +via extensionality that they are equal. + +Contributed by Armin Biere (armin.biere@jku.at). +} +:status unsat +:category { crafted } +:logic QF_AUFBV +:difficulty { 2 } +:extrafuns ((a1 Array[32:8])) +:extrafuns ((v6 BitVec[32])) +:extrafuns ((v7 BitVec[32])) +:extrafuns ((v8 BitVec[32])) +:extrafuns ((v9 BitVec[32])) +:extrafuns ((v10 BitVec[32])) +:extrafuns ((v11 BitVec[32])) +:extrafuns ((v12 BitVec[32])) +:extrafuns ((v13 BitVec[32])) +:extrafuns ((v14 BitVec[32])) +:extrafuns ((v15 BitVec[32])) +:formula +(let (?e2 bv0[32]) +(let (?e3 bv1[32]) +(let (?e4 bv2[32]) +(let (?e5 bv3[32]) +(let (?e16 (bvadd ?e2 v6)) +(let (?e17 (extract[7:0] v6)) +(let (?e18 (store a1 ?e16 ?e17)) +(let (?e19 (bvadd ?e3 v6)) +(let (?e20 (extract[15:8] v6)) +(let (?e21 (store ?e18 ?e19 ?e20)) +(let (?e22 (bvadd ?e4 v6)) +(let (?e23 (extract[23:16] v6)) +(let (?e24 (store ?e21 ?e22 ?e23)) +(let (?e25 (bvadd ?e5 v6)) +(let (?e26 (extract[31:24] v6)) +(let (?e27 (store ?e24 ?e25 ?e26)) +(let (?e28 (bvadd ?e2 v7)) +(let (?e29 (extract[7:0] v7)) +(let (?e30 (store ?e27 ?e28 ?e29)) +(let (?e31 (bvadd ?e3 v7)) +(let (?e32 (extract[15:8] v7)) +(let (?e33 (store ?e30 ?e31 ?e32)) +(let (?e34 (bvadd ?e4 v7)) +(let (?e35 (extract[23:16] v7)) +(let (?e36 (store ?e33 ?e34 ?e35)) +(let (?e37 (bvadd ?e5 v7)) +(let (?e38 (extract[31:24] v7)) +(let (?e39 (store ?e36 ?e37 ?e38)) +(let (?e40 (bvadd ?e2 v8)) +(let (?e41 (extract[7:0] v8)) +(let (?e42 (store ?e39 ?e40 ?e41)) +(let (?e43 (bvadd ?e3 v8)) +(let (?e44 (extract[15:8] v8)) +(let (?e45 (store ?e42 ?e43 ?e44)) +(let (?e46 (bvadd ?e4 v8)) +(let (?e47 (extract[23:16] v8)) +(let (?e48 (store ?e45 ?e46 ?e47)) +(let (?e49 (bvadd ?e5 v8)) +(let (?e50 (extract[31:24] v8)) +(let (?e51 (store ?e48 ?e49 ?e50)) +(let (?e52 (bvadd ?e2 v9)) +(let (?e53 (extract[7:0] v9)) +(let (?e54 (store ?e51 ?e52 ?e53)) +(let (?e55 (bvadd ?e3 v9)) +(let (?e56 (extract[15:8] v9)) +(let (?e57 (store ?e54 ?e55 ?e56)) +(let (?e58 (bvadd ?e4 v9)) +(let (?e59 (extract[23:16] v9)) +(let (?e60 (store ?e57 ?e58 ?e59)) +(let (?e61 (bvadd ?e5 v9)) +(let (?e62 (extract[31:24] v9)) +(let (?e63 (store ?e60 ?e61 ?e62)) +(let (?e64 (bvadd ?e2 v10)) +(let (?e65 (extract[7:0] v10)) +(let (?e66 (store ?e63 ?e64 ?e65)) +(let (?e67 (bvadd ?e3 v10)) +(let (?e68 (extract[15:8] v10)) +(let (?e69 (store ?e66 ?e67 ?e68)) +(let (?e70 (bvadd ?e4 v10)) +(let (?e71 (extract[23:16] v10)) +(let (?e72 (store ?e69 ?e70 ?e71)) +(let (?e73 (bvadd ?e5 v10)) +(let (?e74 (extract[31:24] v10)) +(let (?e75 (store ?e72 ?e73 ?e74)) +(let (?e76 (bvadd ?e2 v11)) +(let (?e77 (extract[7:0] v11)) +(let (?e78 (store ?e75 ?e76 ?e77)) +(let (?e79 (bvadd ?e3 v11)) +(let (?e80 (extract[15:8] v11)) +(let (?e81 (store ?e78 ?e79 ?e80)) +(let (?e82 (bvadd ?e4 v11)) +(let (?e83 (extract[23:16] v11)) +(let (?e84 (store ?e81 ?e82 ?e83)) +(let (?e85 (bvadd ?e5 v11)) +(let (?e86 (extract[31:24] v11)) +(let (?e87 (store ?e84 ?e85 ?e86)) +(let (?e88 (bvadd ?e2 v12)) +(let (?e89 (extract[7:0] v12)) +(let (?e90 (store ?e87 ?e88 ?e89)) +(let (?e91 (bvadd ?e3 v12)) +(let (?e92 (extract[15:8] v12)) +(let (?e93 (store ?e90 ?e91 ?e92)) +(let (?e94 (bvadd ?e4 v12)) +(let (?e95 (extract[23:16] v12)) +(let (?e96 (store ?e93 ?e94 ?e95)) +(let (?e97 (bvadd ?e5 v12)) +(let (?e98 (extract[31:24] v12)) +(let (?e99 (store ?e96 ?e97 ?e98)) +(let (?e100 (bvadd ?e2 v13)) +(let (?e101 (extract[7:0] v13)) +(let (?e102 (store ?e99 ?e100 ?e101)) +(let (?e103 (bvadd ?e3 v13)) +(let (?e104 (extract[15:8] v13)) +(let (?e105 (store ?e102 ?e103 ?e104)) +(let (?e106 (bvadd ?e4 v13)) +(let (?e107 (extract[23:16] v13)) +(let (?e108 (store ?e105 ?e106 ?e107)) +(let (?e109 (bvadd ?e5 v13)) +(let (?e110 (extract[31:24] v13)) +(let (?e111 (store ?e108 ?e109 ?e110)) +(let (?e112 (bvadd ?e2 v14)) +(let (?e113 (extract[7:0] v14)) +(let (?e114 (store ?e111 ?e112 ?e113)) +(let (?e115 (bvadd ?e3 v14)) +(let (?e116 (extract[15:8] v14)) +(let (?e117 (store ?e114 ?e115 ?e116)) +(let (?e118 (bvadd ?e4 v14)) +(let (?e119 (extract[23:16] v14)) +(let (?e120 (store ?e117 ?e118 ?e119)) +(let (?e121 (bvadd ?e5 v14)) +(let (?e122 (extract[31:24] v14)) +(let (?e123 (store ?e120 ?e121 ?e122)) +(let (?e124 (bvadd ?e2 v15)) +(let (?e125 (extract[7:0] v15)) +(let (?e126 (store ?e123 ?e124 ?e125)) +(let (?e127 (bvadd ?e3 v15)) +(let (?e128 (extract[15:8] v15)) +(let (?e129 (store ?e126 ?e127 ?e128)) +(let (?e130 (bvadd ?e4 v15)) +(let (?e131 (extract[23:16] v15)) +(let (?e132 (store ?e129 ?e130 ?e131)) +(let (?e133 (bvadd ?e5 v15)) +(let (?e134 (extract[31:24] v15)) +(let (?e135 (store ?e132 ?e133 ?e134)) +(let (?e136 (store a1 ?e124 ?e125)) +(let (?e137 (store ?e136 ?e127 ?e128)) +(let (?e138 (store ?e137 ?e130 ?e131)) +(let (?e139 (store ?e138 ?e133 ?e134)) +(let (?e140 (store ?e139 ?e112 ?e113)) +(let (?e141 (store ?e140 ?e115 ?e116)) +(let (?e142 (store ?e141 ?e118 ?e119)) +(let (?e143 (store ?e142 ?e121 ?e122)) +(let (?e144 (store ?e143 ?e100 ?e101)) +(let (?e145 (store ?e144 ?e103 ?e104)) +(let (?e146 (store ?e145 ?e106 ?e107)) +(let (?e147 (store ?e146 ?e109 ?e110)) +(let (?e148 (store ?e147 ?e88 ?e89)) +(let (?e149 (store ?e148 ?e91 ?e92)) +(let (?e150 (store ?e149 ?e94 ?e95)) +(let (?e151 (store ?e150 ?e97 ?e98)) +(let (?e152 (store ?e151 ?e76 ?e77)) +(let (?e153 (store ?e152 ?e79 ?e80)) +(let (?e154 (store ?e153 ?e82 ?e83)) +(let (?e155 (store ?e154 ?e85 ?e86)) +(let (?e156 (store ?e155 ?e64 ?e65)) +(let (?e157 (store ?e156 ?e67 ?e68)) +(let (?e158 (store ?e157 ?e70 ?e71)) +(let (?e159 (store ?e158 ?e73 ?e74)) +(let (?e160 (store ?e159 ?e52 ?e53)) +(let (?e161 (store ?e160 ?e55 ?e56)) +(let (?e162 (store ?e161 ?e58 ?e59)) +(let (?e163 (store ?e162 ?e61 ?e62)) +(let (?e164 (store ?e163 ?e40 ?e41)) +(let (?e165 (store ?e164 ?e43 ?e44)) +(let (?e166 (store ?e165 ?e46 ?e47)) +(let (?e167 (store ?e166 ?e49 ?e50)) +(let (?e168 (store ?e167 ?e28 ?e29)) +(let (?e169 (store ?e168 ?e31 ?e32)) +(let (?e170 (store ?e169 ?e34 ?e35)) +(let (?e171 (store ?e170 ?e37 ?e38)) +(let (?e172 (store ?e171 ?e16 ?e17)) +(let (?e173 (store ?e172 ?e19 ?e20)) +(let (?e174 (store ?e173 ?e22 ?e23)) +(let (?e175 (store ?e174 ?e25 ?e26)) +(let (?e176 (ite (= ?e135 ?e175) bv1[1] bv0[1])) +(let (?e177 (extract[1:0] v6)) +(let (?e178 bv0[2]) +(let (?e179 (ite (= ?e177 ?e178) bv1[1] bv0[1])) +(let (?e180 (bvand (bvnot ?e176) ?e179)) +(let (?e181 (extract[1:0] v7)) +(let (?e182 (ite (= ?e178 ?e181) bv1[1] bv0[1])) +(let (?e183 (bvand ?e180 ?e182)) +(let (?e184 (extract[1:0] v8)) +(let (?e185 (ite (= ?e178 ?e184) bv1[1] bv0[1])) +(let (?e186 (bvand ?e183 ?e185)) +(let (?e187 (extract[1:0] v9)) +(let (?e188 (ite (= ?e178 ?e187) bv1[1] bv0[1])) +(let (?e189 (bvand ?e186 ?e188)) +(let (?e190 (extract[1:0] v10)) +(let (?e191 (ite (= ?e178 ?e190) bv1[1] bv0[1])) +(let (?e192 (bvand ?e189 ?e191)) +(let (?e193 (extract[1:0] v11)) +(let (?e194 (ite (= ?e178 ?e193) bv1[1] bv0[1])) +(let (?e195 (bvand ?e192 ?e194)) +(let (?e196 (extract[1:0] v12)) +(let (?e197 (ite (= ?e178 ?e196) bv1[1] bv0[1])) +(let (?e198 (bvand ?e195 ?e197)) +(let (?e199 (extract[1:0] v13)) +(let (?e200 (ite (= ?e178 ?e199) bv1[1] bv0[1])) +(let (?e201 (bvand ?e198 ?e200)) +(let (?e202 (extract[1:0] v14)) +(let (?e203 (ite (= ?e178 ?e202) bv1[1] bv0[1])) +(let (?e204 (bvand ?e201 ?e203)) +(let (?e205 (extract[1:0] v15)) +(let (?e206 (ite (= ?e178 ?e205) bv1[1] bv0[1])) +(let (?e207 (bvand ?e204 ?e206)) +(not (= ?e207 bv0[1])) +))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) diff --git a/test/regress/regress0/auflia/Makefile.am b/test/regress/regress0/auflia/Makefile.am index 314566f87..f4f5c57b4 100644 --- a/test/regress/regress0/auflia/Makefile.am +++ b/test/regress/regress0/auflia/Makefile.am @@ -9,7 +9,8 @@ endif # If a test shouldn't be run in e.g. competition mode, # put it below in "TESTS +=" TESTS = \ - bug336.smt2 + bug330.smt2 \ + bug336.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/bv/Makefile.am b/test/regress/regress0/bv/Makefile.am index 5048ca680..07619b965 100644 --- a/test/regress/regress0/bv/Makefile.am +++ b/test/regress/regress0/bv/Makefile.am @@ -28,7 +28,8 @@ SMT_TESTS = \ fuzz11.smt \ fuzz12.smt \ fuzz13.smt \ - fuzz14.smt + fuzz14.smt \ + calc2_sec2_shifter_mult_bmc15.atlas.delta01.smt # Regression tests for SMT2 inputs SMT2_TESTS = diff --git a/test/regress/regress0/bv/bug345.smt b/test/regress/regress0/bv/bug345.smt new file mode 100644 index 000000000..b836cba2c --- /dev/null +++ b/test/regress/regress0/bv/bug345.smt @@ -0,0 +1,46 @@ +(benchmark B_ +:logic QF_AUFBV +:extrafuns ((mem_35_197 Array[32:8])) +:status unknown +:formula +(let (?n1 bv1[1]) +(let (?n2 bv0[31]) +(let (?n3 bv0[32]) +(let (?n4 bv0[24]) +(let (?n5 (select mem_35_197 ?n3)) +(let (?n6 (concat ?n4 ?n5)) +(flet ($n7 (= ?n3 ?n6)) +(let (?n8 bv0[1]) +(let (?n9 (ite $n7 ?n1 ?n8)) +(let (?n10 (concat ?n2 ?n9)) +(let (?n11 (extract[0:0] ?n10)) +(let (?n12 bv0[8]) +(let (?n13 bv1[32]) +(let (?n14 (select mem_35_197 ?n13)) +(let (?n15 (concat ?n4 ?n14)) +(let (?n16 (extract[7:0] ?n15)) +(flet ($n17 (= ?n12 ?n16)) +(let (?n18 bv1[8]) +(flet ($n19 (= ?n16 ?n18)) +(let (?n20 bv3[8]) +(flet ($n21 (= ?n16 ?n20)) +(let (?n22 (ite $n21 ?n13 ?n3)) +(let (?n23 (ite $n19 ?n3 ?n22)) +(let (?n24 (ite $n17 ?n13 ?n23)) +(let (?n25 (extract[7:0] ?n24)) +(let (?n26 (store mem_35_197 ?n3 ?n25)) +(let (?n27 (concat ?n4 ?n16)) +(let (?n28 (extract[7:0] ?n27)) +(let (?n29 (concat ?n4 ?n28)) +(let (?n30 (extract[7:0] ?n29)) +(let (?n31 (concat ?n4 ?n30)) +(let (?n32 (bvadd ?n6 ?n31)) +(let (?n33 (store ?n26 ?n32 ?n12)) +(let (?n34 (select ?n33 ?n3)) +(let (?n35 (concat ?n4 ?n34)) +(flet ($n36 (= ?n3 ?n35)) +(let (?n37 (ite $n36 ?n1 ?n8)) +(let (?n38 (bvor ?n11 ?n37)) +(flet ($n39 (= ?n1 ?n38)) +$n39 +)))))))))))))))))))))))))))))))))))))))) diff --git a/test/regress/regress0/bv/calc2_sec2_shifter_mult_bmc15.atlas.delta01.smt b/test/regress/regress0/bv/calc2_sec2_shifter_mult_bmc15.atlas.delta01.smt new file mode 100644 index 000000000..467f10c39 --- /dev/null +++ b/test/regress/regress0/bv/calc2_sec2_shifter_mult_bmc15.atlas.delta01.smt @@ -0,0 +1,80 @@ +(benchmark B_ +:logic QF_BV +:extrapreds ((UCL_p16)) +:extrapreds ((UCL_p34)) +:status sat +:formula +(let (?n1 bv1[1]) +(let (?n2 bv0[2]) +(let (?n3 bv1[5]) +(let (?n4 bv0[5]) +(let (?n5 bv0[4]) +(let (?n6 bv1[4]) +(let (?n7 (ite UCL_p16 ?n6 ?n5)) +(flet ($n8 (= ?n5 ?n7)) +(let (?n9 bv1[2]) +(let (?n10 (ite $n8 ?n9 ?n2)) +(flet ($n11 (= ?n2 ?n10)) +(flet ($n12 (= ?n9 ?n10)) +(flet ($n13 (or $n11 $n12)) +(let (?n14 (ite $n13 ?n3 ?n4)) +(flet ($n15 (= ?n4 ?n14)) +(let (?n16 (ite $n15 ?n3 ?n4)) +(flet ($n17 (= ?n4 ?n16)) +(let (?n18 (ite UCL_p34 ?n2 ?n9)) +(flet ($n19 (= ?n9 ?n18)) +(let (?n20 (ite $n19 ?n6 ?n5)) +(flet ($n21 (= ?n5 ?n20)) +(let (?n22 (ite $n21 ?n3 ?n4)) +(let (?n23 (bvadd ?n22 ?n16)) +(let (?n24 (bvadd ?n3 ?n23)) +(let (?n25 (ite $n17 ?n24 ?n23)) +(flet ($n26 (= ?n3 ?n25)) +(let (?n27 bv1[6]) +(let (?n28 (concat ?n27 ?n9)) +(let (?n29 bv0[32]) +(let (?n30 (concat ?n28 ?n29)) +(let (?n31 (concat ?n30 ?n29)) +(let (?n32 bv0[72]) +(let (?n33 (ite $n26 ?n31 ?n32)) +(let (?n34 (extract[67:64] ?n33)) +(let (?n35 (extract[3:2] ?n34)) +(flet ($n36 (= ?n2 ?n35)) +(let (?n37 (ite $n36 ?n9 ?n2)) +(flet ($n38 (= ?n2 ?n37)) +(let (?n39 bv0[3]) +(let (?n40 bv1[3]) +(let (?n41 (ite $n38 ?n39 ?n40)) +(let (?n42 (extract[0:0] ?n41)) +(flet ($n43 (= ?n1 ?n42)) +(let (?n44 (ite $n43 ?n9 ?n2)) +(let (?n45 (ite $n12 ?n3 ?n4)) +(flet ($n46 (= ?n4 ?n45)) +(let (?n47 (ite $n8 ?n3 ?n4)) +(flet ($n48 (= ?n4 ?n47)) +(let (?n49 (ite $n48 ?n14 ?n4)) +(flet ($n50 (= ?n4 ?n49)) +(let (?n51 (bvsub ?n4 ?n3)) +(let (?n52 (ite $n50 ?n4 ?n51)) +(flet ($n53 (= ?n4 ?n52)) +(let (?n54 (ite $n53 ?n3 ?n52)) +(let (?n55 (ite $n46 ?n4 ?n54)) +(flet ($n56 (= ?n3 ?n55)) +(let (?n57 (concat ?n6 ?n9)) +(let (?n58 (concat ?n57 ?n2)) +(let (?n59 (concat ?n58 ?n29)) +(let (?n60 (concat ?n59 ?n29)) +(let (?n61 (bvadd ?n45 ?n52)) +(flet ($n62 (= ?n3 ?n61)) +(let (?n63 (ite $n62 ?n32 ?n31)) +(let (?n64 (ite $n56 ?n60 ?n63)) +(let (?n65 (extract[67:64] ?n64)) +(let (?n66 (extract[3:2] ?n65)) +(flet ($n67 (= ?n2 ?n66)) +(let (?n68 (extract[71:68] ?n64)) +(flet ($n69 (= ?n5 ?n68)) +(let (?n70 (ite $n69 ?n2 ?n9)) +(let (?n71 (ite $n67 ?n70 ?n2)) +(flet ($n72 (= ?n44 ?n71)) +$n72 +))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) diff --git a/test/regress/regress0/uflia/Makefile.am b/test/regress/regress0/uflia/Makefile.am index 0244d768e..5b095b500 100644 --- a/test/regress/regress0/uflia/Makefile.am +++ b/test/regress/regress0/uflia/Makefile.am @@ -14,7 +14,12 @@ MAKEFLAGS = -k # Regression tests for SMT inputs SMT_TESTS = \ xs-09-16-3-4-1-5.smt \ + xs-09-16-3-4-1-5.delta01.smt \ + xs-09-16-3-4-1-5.delta02.smt \ + xs-09-16-3-4-1-5.delta03.smt \ + xs-09-16-3-4-1-5.delta04.smt \ error0.smt2 \ + error0.delta01.smt \ simple_cyclic2.smt2 # Regression tests for SMT2 inputs diff --git a/test/regress/regress0/uflia/error0.delta01.smt b/test/regress/regress0/uflia/error0.delta01.smt new file mode 100644 index 000000000..cc205063c --- /dev/null +++ b/test/regress/regress0/uflia/error0.delta01.smt @@ -0,0 +1,78 @@ +(benchmark B_ +:logic QF_UFLIA +:extrafuns ((format Int Int)) +:extrafuns ((arg1 Int)) +:extrafuns ((fmt1 Int)) +:extrafuns ((s_count Int Int)) +:extrafuns ((fmt0 Int)) +:extrafuns ((x_count Int Int)) +:status sat +:formula +(flet ($n1 true) +(let (?n2 1) +(let (?n3 (~ ?n2)) +(let (?n4 (* ?n3 fmt1)) +(let (?n5 (+ ?n4 fmt0)) +(let (?n6 8) +(let (?n7 (~ ?n6)) +(flet ($n8 (>= ?n5 ?n7)) +(let (?n9 6) +(let (?n10 (x_count ?n9)) +(let (?n11 7) +(let (?n12 (x_count ?n11)) +(let (?n13 (* ?n3 ?n12)) +(let (?n14 (+ ?n10 ?n13)) +(let (?n15 0) +(flet ($n16 (>= ?n14 ?n15)) +(flet ($n17 (>= fmt1 ?n11)) +(flet ($n18 (<= arg1 ?n9)) +(let (?n19 2) +(let (?n20 (~ ?n19)) +(let (?n21 (* ?n3 fmt0)) +(let (?n22 (+ fmt1 ?n20 ?n21)) +(let (?n23 (s_count ?n22)) +(let (?n24 5) +(let (?n25 (s_count ?n24)) +(let (?n26 (* ?n3 ?n25)) +(let (?n27 (+ ?n23 ?n26)) +(flet ($n28 (= ?n15 ?n27)) +(flet ($n29 (not $n28)) +(let (?n30 (~ ?n11)) +(flet ($n31 (<= ?n5 ?n30)) +(flet ($n32 false) +(let (?n33 (+ arg1 ?n21)) +(flet ($n34 (<= ?n33 ?n2)) +(let (?n35 (+ ?n4 arg1)) +(flet ($n36 (<= ?n35 ?n15)) +(flet ($n37 (or $n32 $n32 $n34 $n36)) +(let (?n38 (x_count ?n2)) +(flet ($n39 (>= ?n38 ?n15)) +(let (?n40 (format ?n11)) +(flet ($n41 (<= ?n40 ?n15)) +(let (?n42 (x_count ?n22)) +(let (?n43 (+ ?n13 ?n42)) +(flet ($n44 (= ?n15 ?n43)) +(let (?n45 (s_count ?n9)) +(let (?n46 (* ?n3 ?n45)) +(let (?n47 (+ ?n23 ?n46)) +(flet ($n48 (= ?n15 ?n47)) +(flet ($n49 (or $n32 $n32 $n32 $n32 $n32 $n39 $n44 $n48)) +(let (?n50 (+ ?n2 fmt1)) +(let (?n51 (format ?n50)) +(flet ($n52 (>= ?n51 ?n15)) +(let (?n53 4) +(let (?n54 (format ?n53)) +(flet ($n55 (>= ?n54 ?n15)) +(let (?n56 9) +(let (?n57 (format ?n56)) +(flet ($n58 (<= ?n57 ?n15)) +(let (?n59 (format fmt1)) +(flet ($n60 (>= ?n59 ?n15)) +(let (?n61 12) +(let (?n62 (format ?n61)) +(flet ($n63 (>= ?n62 ?n15)) +(let (?n64 (format arg1)) +(flet ($n65 (= ?n15 ?n64)) +(flet ($n66 (and $n1 $n8 $n16 $n17 $n18 $n29 $n31 $n37 $n39 $n41 $n49 $n52 $n55 $n58 $n60 $n63 $n65)) +$n66 +))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) diff --git a/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta01.smt b/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta01.smt new file mode 100644 index 000000000..c7fed0c15 --- /dev/null +++ b/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta01.smt @@ -0,0 +1,48 @@ +(benchmark mathsat +:logic QF_UFLIA +:extrafuns ((s_count Int Int)) +:extrafuns ((fmt1 Int)) +:extrafuns ((fmt_length Int)) +:status unsat +:formula +(let (?n1 0) +(let (?n2 6) +(let (?n3 (s_count ?n2)) +(flet ($n4 (= ?n1 ?n3)) +(let (?n5 5) +(let (?n6 (s_count ?n5)) +(flet ($n7 (= ?n1 ?n6)) +(let (?n8 4) +(let (?n9 (s_count ?n8)) +(flet ($n10 (= ?n1 ?n9)) +(let (?n11 3) +(let (?n12 (s_count ?n11)) +(flet ($n13 (= ?n1 ?n12)) +(let (?n14 1) +(let (?n15 (s_count ?n1)) +(flet ($n16 (= ?n14 ?n15)) +(let (?n17 (s_count ?n14)) +(flet ($n18 (= ?n1 ?n17)) +(flet ($n19 (and $n16 $n18)) +(let (?n20 2) +(let (?n21 (s_count ?n20)) +(flet ($n22 (= ?n1 ?n21)) +(flet ($n23 (and $n19 $n22)) +(flet ($n24 (and $n13 $n23)) +(flet ($n25 (and $n10 $n24)) +(flet ($n26 (and $n7 $n25)) +(flet ($n27 (and $n4 $n26)) +(let (?n28 9) +(flet ($n29 (= ?n28 fmt_length)) +(flet ($n30 (> fmt1 ?n14)) +(flet ($n31 (< fmt1 fmt_length)) +(flet ($n32 (and $n30 $n31)) +(let (?n33 (- fmt1 ?n20)) +(let (?n34 (s_count ?n33)) +(let (?n35 (+ ?n14 ?n34)) +(flet ($n36 (= ?n1 ?n35)) +(flet ($n37 (and $n32 $n36)) +(flet ($n38 (and $n29 $n37)) +(flet ($n39 (and $n27 $n38)) +$n39 +)))))))))))))))))))))))))))))))))))))))) diff --git a/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta02.smt b/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta02.smt new file mode 100644 index 000000000..fb16651ff --- /dev/null +++ b/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta02.smt @@ -0,0 +1,40 @@ +(benchmark mathsat +:logic QF_UFLIA +:extrafuns ((arg1 Int)) +:extrafuns ((adr_lo Int)) +:extrafuns ((select_format Int Int)) +:extrafuns ((x Int)) +:status sat +:formula +(let (?n1 (select_format arg1)) +(flet ($n2 (= ?n1 adr_lo)) +(let (?n3 0) +(flet ($n4 (= ?n3 x)) +(let (?n5 4) +(let (?n6 (select_format ?n5)) +(flet ($n7 (= adr_lo ?n6)) +(let (?n8 3) +(let (?n9 (select_format ?n8)) +(flet ($n10 (= adr_lo ?n9)) +(let (?n11 2) +(let (?n12 (select_format ?n11)) +(flet ($n13 (= adr_lo ?n12)) +(let (?n14 1) +(let (?n15 (select_format ?n3)) +(flet ($n16 (= ?n14 ?n15)) +(let (?n17 (select_format ?n14)) +(flet ($n18 (= ?n3 ?n17)) +(flet ($n19 (or $n16 $n18)) +(flet ($n20 (or $n13 $n19)) +(flet ($n21 (or $n10 $n20)) +(flet ($n22 (or $n7 $n21)) +(flet ($n23 (or $n4 $n22)) +(flet ($n24 (= adr_lo ?n8)) +(flet ($n25 (< arg1 ?n5)) +(flet ($n26 (>= arg1 ?n3)) +(flet ($n27 (and $n25 $n26)) +(flet ($n28 (and $n24 $n27)) +(flet ($n29 (and $n23 $n28)) +(flet ($n30 (and $n2 $n29)) +$n30 +))))))))))))))))))))))))))))))) diff --git a/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta03.smt b/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta03.smt new file mode 100644 index 000000000..6f65e83ec --- /dev/null +++ b/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta03.smt @@ -0,0 +1,45 @@ +(benchmark mathsat +:logic QF_UFLIA +:extrafuns ((fmt_length Int)) +:extrafuns ((fmt1 Int)) +:extrafuns ((arg1 Int)) +:extrafuns ((select_format Int Int)) +:status sat +:formula +(let (?n1 1) +(let (?n2 (+ ?n1 fmt1)) +(let (?n3 (select_format ?n2)) +(flet ($n4 (= ?n1 ?n3)) +(let (?n5 (select_format arg1)) +(let (?n6 0) +(flet ($n7 (= ?n5 ?n6)) +(flet ($n8 (and $n4 $n7)) +(let (?n9 7) +(let (?n10 (select_format ?n9)) +(flet ($n11 (= ?n1 ?n10)) +(let (?n12 (select_format ?n6)) +(flet ($n13 (= ?n1 ?n12)) +(let (?n14 (select_format ?n1)) +(flet ($n15 (= ?n1 ?n14)) +(flet ($n16 (or $n13 $n15)) +(let (?n17 5) +(let (?n18 (select_format ?n17)) +(flet ($n19 (= ?n6 ?n18)) +(flet ($n20 (or $n16 $n19)) +(let (?n21 6) +(let (?n22 (select_format ?n21)) +(flet ($n23 (= ?n6 ?n22)) +(flet ($n24 (or $n20 $n23)) +(flet ($n25 (or $n11 $n24)) +(let (?n26 9) +(flet ($n27 (= ?n26 fmt_length)) +(let (?n28 2) +(let (?n29 (- fmt1 ?n28)) +(flet ($n30 (= arg1 ?n29)) +(flet ($n31 (< fmt1 fmt_length)) +(flet ($n32 (and $n30 $n31)) +(flet ($n33 (and $n27 $n32)) +(flet ($n34 (and $n25 $n33)) +(flet ($n35 (and $n8 $n34)) +$n35 +)))))))))))))))))))))))))))))))))))) diff --git a/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta04.smt b/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta04.smt new file mode 100644 index 000000000..f1212a876 --- /dev/null +++ b/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta04.smt @@ -0,0 +1,67 @@ +(benchmark mathsat +:logic QF_UFLIA +:extrafuns ((fmt_length Int)) +:extrafuns ((fmt1 Int)) +:extrafuns ((x_count Int Int)) +:extrafuns ((select_format Int Int)) +:extrafuns ((percent Int)) +:extrafuns ((s_count Int Int)) +:status sat +:formula +(let (?n1 1) +(let (?n2 5) +(let (?n3 (x_count ?n2)) +(flet ($n4 (= ?n1 ?n3)) +(let (?n5 4) +(let (?n6 (x_count ?n5)) +(flet ($n7 (= ?n1 ?n6)) +(let (?n8 3) +(let (?n9 (x_count ?n8)) +(let (?n10 2) +(let (?n11 (x_count ?n10)) +(flet ($n12 (= ?n9 ?n11)) +(let (?n13 0) +(let (?n14 (select_format ?n8)) +(flet ($n15 (= ?n13 ?n14)) +(let (?n16 (x_count ?n13)) +(flet ($n17 (= ?n1 ?n16)) +(flet ($n18 (= ?n1 percent)) +(flet ($n19 true) +(let (?n20 (s_count ?n13)) +(flet ($n21 (= ?n13 ?n20)) +(flet ($n22 (if_then_else $n18 $n19 $n21)) +(let (?n23 (select_format ?n10)) +(flet ($n24 (= percent ?n23)) +(flet ($n25 (= ?n1 ?n14)) +(flet ($n26 (and $n24 $n25)) +(flet ($n27 false) +(flet ($n28 (if_then_else $n26 $n27 $n19)) +(flet ($n29 (and $n22 $n28)) +(flet ($n30 (and $n17 $n29)) +(flet ($n31 (= ?n13 percent)) +(flet ($n32 (= ?n13 ?n23)) +(flet ($n33 (and $n31 $n32)) +(let (?n34 (x_count ?n1)) +(flet ($n35 (= ?n13 ?n34)) +(flet ($n36 (= ?n16 ?n34)) +(flet ($n37 (if_then_else $n33 $n35 $n36)) +(flet ($n38 (and $n30 $n37)) +(flet ($n39 (and $n15 $n38)) +(flet ($n40 (and $n12 $n39)) +(flet ($n41 (and $n7 $n40)) +(flet ($n42 (and $n4 $n41)) +(let (?n43 9) +(flet ($n44 (= ?n43 fmt_length)) +(let (?n45 (- fmt1 ?n10)) +(let (?n46 (x_count ?n45)) +(let (?n47 (+ ?n1 ?n46)) +(flet ($n48 (= ?n13 ?n47)) +(flet ($n49 (> fmt1 ?n1)) +(let (?n50 (- fmt_length ?n1)) +(flet ($n51 (< fmt1 ?n50)) +(flet ($n52 (and $n49 $n51)) +(flet ($n53 (and $n48 $n52)) +(flet ($n54 (and $n44 $n53)) +(flet ($n55 (and $n42 $n54)) +$n55 +)))))))))))))))))))))))))))))))))))))))))))))))))))))))) diff --git a/test/system/boilerplate.cpp b/test/system/boilerplate.cpp index c64c1463e..f1dc77988 100644 --- a/test/system/boilerplate.cpp +++ b/test/system/boilerplate.cpp @@ -31,7 +31,8 @@ int main() { ExprManager em; Options opts; SmtEngine smt(&em); - Result r = smt.query(em.mkConst(true)); + BoolExpr F = em.mkConst(true); + Result r = smt.query(F); return r == Result::VALID ? 0 : 1; } diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h index 1de3854b9..34536445f 100644 --- a/test/unit/theory/theory_black.h +++ b/test/unit/theory/theory_black.h @@ -57,9 +57,10 @@ public: push(CONFLICT, n); } - void propagate(TNode n) + bool propagate(TNode n) throw(AssertionException) { push(PROPAGATE, n); + return true; } void propagateAsDecision(TNode n) diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h index ff6cba936..2d6730949 100644 --- a/test/unit/theory/theory_engine_white.h +++ b/test/unit/theory/theory_engine_white.h @@ -51,7 +51,7 @@ class FakeOutputChannel : public OutputChannel { void conflict(TNode n) throw(AssertionException) { Unimplemented(); } - void propagate(TNode n) throw(AssertionException) { + bool propagate(TNode n) throw(AssertionException) { Unimplemented(); } void propagateAsDecision(TNode n) throw(AssertionException) { |