diff options
| author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-06-06 06:12:40 +0000 |
|---|---|---|
| committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-06-06 06:12:40 +0000 |
| commit | fd9e22c4a2e57c3dfeda4de3842a3fb3ca4776ba (patch) | |
| tree | 047e4d27f725e9157ed5bef5357d0d72560218ae /test/regress/regress0/aufbv | |
| parent | 2799ae1cf57ed2b98387a1de1325bccd89bd2a30 (diff) | |
Changes to the combination mechanism, lots of details. Not done yet, there are still the AUFBV wrong results, but it seems better.
http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=4382&reference_id=4359&p=5
Diffstat (limited to 'test/regress/regress0/aufbv')
7 files changed, 1002 insertions, 1 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])) +))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) |