diff options
Diffstat (limited to 'test/regress/regress1/proj-issue175.smt2')
| -rw-r--r-- | test/regress/regress1/proj-issue175.smt2 | 83 |
1 files changed, 83 insertions, 0 deletions
diff --git a/test/regress/regress1/proj-issue175.smt2 b/test/regress/regress1/proj-issue175.smt2 new file mode 100644 index 000000000..2df1e21e6 --- /dev/null +++ b/test/regress/regress1/proj-issue175.smt2 @@ -0,0 +1,83 @@ +(set-logic QF_AUFNIA) +(set-info :status sat) +(declare-fun |#offset~STRUCT#?type~INT?length~UINT?off~UINT?data~$Pointer$?input~$Pointer$?comp~$Pointer$#~data| () Int) +(declare-fun |ssl3_accept_#t~mem38_491| () Int) +(declare-fun |#offset~STRUCT#?version~INT?type~INT?method~$Pointer$?rbio~$Pointer$?wbio~$Pointer$?bbio~$Pointer$?rwstate~INT?in_handshake~INT?handshake_func~$Pointer$?server~INT?new_session~INT?quiet_shutdown~INT?shutdown~INT?state~INT?rstate~INT?init_buf~$Pointer$?init_num~INT?init_off~INT?packet~$Pointer$?packet_length~UINT?s2~$Pointer$?s3~$Pointer$?read_ahead~INT?hit~INT?purpose~INT?trust~INT?cipher_list~$Pointer$?cipher_list_by_id~$Pointer$?enc_read_ctx~$Pointer$?read_hash~$Pointer$?expand~$Pointer$?enc_write_ctx~$Pointer$?write_hash~$Pointer$?compress~$Pointer$?cert~$Pointer$?sid_ctx_length~UINT?sid_ctx~ARRAY#_32_~UCHAR#?session~$Pointer$?verify_mode~INT?verify_depth~INT?verify_callback~$Pointer$?info_callback~$Pointer$?error~INT?error_code~INT?ctx~$Pointer$?debug~INT?verify_result~LONG?ex_data~~CRYPTO_EX_DATA?client_CA~$Pointer$?references~INT?options~ULONG?mode~ULONG?first_packet~INT?client_version~INT#~state| () Int) +(declare-fun ssl3_accept_~s.offset_12 () Int) +(declare-fun ssl3_accept_~s.base_12 () Int) +(declare-fun |#memory_int_136| () (Array Int (Array Int Int))) +(declare-fun |ssl3_accept_#t~mem35_173| () Int) +(declare-fun |ssl3_accept_#t~mem49_513| () Int) +(declare-fun |ssl3_accept_#t~mem29_161| () Int) +(declare-fun |#memory_int_53| () (Array Int (Array Int Int))) +(declare-fun |ssl3_accept_#t~mem24_68| () Int) +(declare-fun |#memory_int_601| () (Array Int (Array Int Int))) +(declare-fun |ssl3_accept_#t~mem31_631| () Int) +(declare-fun |#offset~STRUCT#?version~INT?type~INT?method~$Pointer$?rbio~$Pointer$?wbio~$Pointer$?bbio~$Pointer$?rwstate~INT?in_handshake~INT?handshake_func~$Pointer$?server~INT?new_session~INT?quiet_shutdown~INT?shutdown~INT?state~INT?rstate~INT?init_buf~$Pointer$?init_num~INT?init_off~INT?packet~$Pointer$?packet_length~UINT?s2~$Pointer$?s3~$Pointer$?read_ahead~INT?hit~INT?purpose~INT?trust~INT?cipher_list~$Pointer$?cipher_list_by_id~$Pointer$?enc_read_ctx~$Pointer$?read_hash~$Pointer$?expand~$Pointer$?enc_write_ctx~$Pointer$?write_hash~$Pointer$?compress~$Pointer$?cert~$Pointer$?sid_ctx_length~UINT?sid_ctx~ARRAY#_32_~UCHAR#?session~$Pointer$?verify_mode~INT?verify_depth~INT?verify_callback~$Pointer$?info_callback~$Pointer$?error~INT?error_code~INT?ctx~$Pointer$?debug~INT?verify_result~LONG?ex_data~~CRYPTO_EX_DATA?client_CA~$Pointer$?references~INT?options~ULONG?mode~ULONG?first_packet~INT?client_version~INT#~init_num| () Int) +(declare-fun |#memory_$Pointer$.base_53| () (Array Int (Array Int Int))) +(declare-fun |#memory_$Pointer$.base_52| () (Array Int (Array Int Int))) +(declare-fun |ssl3_accept_#t~nondet159_515| () Int) +(declare-fun ssl3_accept_~ret~10_753 () Int) +(declare-fun ssl3_accept_~ret~10_314 () Int) +(declare-fun |ssl3_accept_#t~mem22_459| () Int) +(declare-fun |#offset~STRUCT#?version~INT?type~INT?method~$Pointer$?rbio~$Pointer$?wbio~$Pointer$?bbio~$Pointer$?rwstate~INT?in_handshake~INT?handshake_func~$Pointer$?server~INT?new_session~INT?quiet_shutdown~INT?shutdown~INT?state~INT?rstate~INT?init_buf~$Pointer$?init_num~INT?init_off~INT?packet~$Pointer$?packet_length~UINT?s2~$Pointer$?s3~$Pointer$?read_ahead~INT?hit~INT?purpose~INT?trust~INT?cipher_list~$Pointer$?cipher_list_by_id~$Pointer$?enc_read_ctx~$Pointer$?read_hash~$Pointer$?expand~$Pointer$?enc_write_ctx~$Pointer$?write_hash~$Pointer$?compress~$Pointer$?cert~$Pointer$?sid_ctx_length~UINT?sid_ctx~ARRAY#_32_~UCHAR#?session~$Pointer$?verify_mode~INT?verify_depth~INT?verify_callback~$Pointer$?info_callback~$Pointer$?error~INT?error_code~INT?ctx~$Pointer$?debug~INT?verify_result~LONG?ex_data~~CRYPTO_EX_DATA?client_CA~$Pointer$?references~INT?options~ULONG?mode~ULONG?first_packet~INT?client_version~INT#~s3| () Int) +(declare-fun |#memory_$Pointer$.offset_521| () (Array Int (Array Int Int))) +(declare-fun |ssl3_accept_#t~mem165.offset_593| () Int) +(declare-fun |ssl3_accept_#t~mem23_461| () Int) +(declare-fun |#offset~STRUCT#?version~INT?type~INT?method~$Pointer$?rbio~$Pointer$?wbio~$Pointer$?bbio~$Pointer$?rwstate~INT?in_handshake~INT?handshake_func~$Pointer$?server~INT?new_session~INT?quiet_shutdown~INT?shutdown~INT?state~INT?rstate~INT?init_buf~$Pointer$?init_num~INT?init_off~INT?packet~$Pointer$?packet_length~UINT?s2~$Pointer$?s3~$Pointer$?read_ahead~INT?hit~INT?purpose~INT?trust~INT?cipher_list~$Pointer$?cipher_list_by_id~$Pointer$?enc_read_ctx~$Pointer$?read_hash~$Pointer$?expand~$Pointer$?enc_write_ctx~$Pointer$?write_hash~$Pointer$?compress~$Pointer$?cert~$Pointer$?sid_ctx_length~UINT?sid_ctx~ARRAY#_32_~UCHAR#?session~$Pointer$?verify_mode~INT?verify_depth~INT?verify_callback~$Pointer$?info_callback~$Pointer$?error~INT?error_code~INT?ctx~$Pointer$?debug~INT?verify_result~LONG?ex_data~~CRYPTO_EX_DATA?client_CA~$Pointer$?references~INT?options~ULONG?mode~ULONG?first_packet~INT?client_version~INT#~packet| () Int) +(assert + (let (($x220 (= |#offset~STRUCT#?type~INT?length~UINT?off~UINT?data~$Pointer$?input~$Pointer$?comp~$Pointer$#~data| 12))) + (let (($x2621 (= |ssl3_accept_#t~mem38_491| 8544))) + (let (($x2622 (not $x2621))) + (let (($x10875 (not $x2622))) + (let (($x23085 (and $x10875 $x220))) + (not $x23085))))))) +(assert + (let ((?x806 (+ ssl3_accept_~s.offset_12 |#offset~STRUCT#?version~INT?type~INT?method~$Pointer$?rbio~$Pointer$?wbio~$Pointer$?bbio~$Pointer$?rwstate~INT?in_handshake~INT?handshake_func~$Pointer$?server~INT?new_session~INT?quiet_shutdown~INT?shutdown~INT?state~INT?rstate~INT?init_buf~$Pointer$?init_num~INT?init_off~INT?packet~$Pointer$?packet_length~UINT?s2~$Pointer$?s3~$Pointer$?read_ahead~INT?hit~INT?purpose~INT?trust~INT?cipher_list~$Pointer$?cipher_list_by_id~$Pointer$?enc_read_ctx~$Pointer$?read_hash~$Pointer$?expand~$Pointer$?enc_write_ctx~$Pointer$?write_hash~$Pointer$?compress~$Pointer$?cert~$Pointer$?sid_ctx_length~UINT?sid_ctx~ARRAY#_32_~UCHAR#?session~$Pointer$?verify_mode~INT?verify_depth~INT?verify_callback~$Pointer$?info_callback~$Pointer$?error~INT?error_code~INT?ctx~$Pointer$?debug~INT?verify_result~LONG?ex_data~~CRYPTO_EX_DATA?client_CA~$Pointer$?references~INT?options~ULONG?mode~ULONG?first_packet~INT?client_version~INT#~state|))) + (let ((?x1399 (select |#memory_int_136| ssl3_accept_~s.base_12))) + (let ((?x1400 (select ?x1399 ?x806))) + (let (($x1478 (>= |ssl3_accept_#t~mem35_173| ?x1400))) + (not $x1478)))))) +(assert + (let (($x2678 (>= |ssl3_accept_#t~mem49_513| 8640))) + (not $x2678))) +(assert + (let ((?x806 (+ ssl3_accept_~s.offset_12 |#offset~STRUCT#?version~INT?type~INT?method~$Pointer$?rbio~$Pointer$?wbio~$Pointer$?bbio~$Pointer$?rwstate~INT?in_handshake~INT?handshake_func~$Pointer$?server~INT?new_session~INT?quiet_shutdown~INT?shutdown~INT?state~INT?rstate~INT?init_buf~$Pointer$?init_num~INT?init_off~INT?packet~$Pointer$?packet_length~UINT?s2~$Pointer$?s3~$Pointer$?read_ahead~INT?hit~INT?purpose~INT?trust~INT?cipher_list~$Pointer$?cipher_list_by_id~$Pointer$?enc_read_ctx~$Pointer$?read_hash~$Pointer$?expand~$Pointer$?enc_write_ctx~$Pointer$?write_hash~$Pointer$?compress~$Pointer$?cert~$Pointer$?sid_ctx_length~UINT?sid_ctx~ARRAY#_32_~UCHAR#?session~$Pointer$?verify_mode~INT?verify_depth~INT?verify_callback~$Pointer$?info_callback~$Pointer$?error~INT?error_code~INT?ctx~$Pointer$?debug~INT?verify_result~LONG?ex_data~~CRYPTO_EX_DATA?client_CA~$Pointer$?references~INT?options~ULONG?mode~ULONG?first_packet~INT?client_version~INT#~state|))) + (let ((?x1399 (select |#memory_int_136| ssl3_accept_~s.base_12))) + (let ((?x1400 (select ?x1399 ?x806))) + (let (($x1447 (<= |ssl3_accept_#t~mem29_161| ?x1400))) + (let ((?x1089 (select |#memory_int_53| ssl3_accept_~s.base_12))) + (let ((?x1090 (select ?x1089 ?x806))) + (let (($x1113 (>= |ssl3_accept_#t~mem24_68| ?x1090))) + (let (($x19982 (and $x1113 $x1447))) + (not $x19982)))))))))) +(assert + (let ((?x806 (+ ssl3_accept_~s.offset_12 |#offset~STRUCT#?version~INT?type~INT?method~$Pointer$?rbio~$Pointer$?wbio~$Pointer$?bbio~$Pointer$?rwstate~INT?in_handshake~INT?handshake_func~$Pointer$?server~INT?new_session~INT?quiet_shutdown~INT?shutdown~INT?state~INT?rstate~INT?init_buf~$Pointer$?init_num~INT?init_off~INT?packet~$Pointer$?packet_length~UINT?s2~$Pointer$?s3~$Pointer$?read_ahead~INT?hit~INT?purpose~INT?trust~INT?cipher_list~$Pointer$?cipher_list_by_id~$Pointer$?enc_read_ctx~$Pointer$?read_hash~$Pointer$?expand~$Pointer$?enc_write_ctx~$Pointer$?write_hash~$Pointer$?compress~$Pointer$?cert~$Pointer$?sid_ctx_length~UINT?sid_ctx~ARRAY#_32_~UCHAR#?session~$Pointer$?verify_mode~INT?verify_depth~INT?verify_callback~$Pointer$?info_callback~$Pointer$?error~INT?error_code~INT?ctx~$Pointer$?debug~INT?verify_result~LONG?ex_data~~CRYPTO_EX_DATA?client_CA~$Pointer$?references~INT?options~ULONG?mode~ULONG?first_packet~INT?client_version~INT#~state|))) + (let ((?x3029 (select |#memory_int_601| ssl3_accept_~s.base_12))) + (let ((?x3030 (select ?x3029 ?x806))) + (let (($x3088 (>= |ssl3_accept_#t~mem31_631| ?x3030))) + (let ((?x1050 (+ ssl3_accept_~s.offset_12 |#offset~STRUCT#?version~INT?type~INT?method~$Pointer$?rbio~$Pointer$?wbio~$Pointer$?bbio~$Pointer$?rwstate~INT?in_handshake~INT?handshake_func~$Pointer$?server~INT?new_session~INT?quiet_shutdown~INT?shutdown~INT?state~INT?rstate~INT?init_buf~$Pointer$?init_num~INT?init_off~INT?packet~$Pointer$?packet_length~UINT?s2~$Pointer$?s3~$Pointer$?read_ahead~INT?hit~INT?purpose~INT?trust~INT?cipher_list~$Pointer$?cipher_list_by_id~$Pointer$?enc_read_ctx~$Pointer$?read_hash~$Pointer$?expand~$Pointer$?enc_write_ctx~$Pointer$?write_hash~$Pointer$?compress~$Pointer$?cert~$Pointer$?sid_ctx_length~UINT?sid_ctx~ARRAY#_32_~UCHAR#?session~$Pointer$?verify_mode~INT?verify_depth~INT?verify_callback~$Pointer$?info_callback~$Pointer$?error~INT?error_code~INT?ctx~$Pointer$?debug~INT?verify_result~LONG?ex_data~~CRYPTO_EX_DATA?client_CA~$Pointer$?references~INT?options~ULONG?mode~ULONG?first_packet~INT?client_version~INT#~init_num|))) + (let ((?x1051 (select |#memory_$Pointer$.base_53| ssl3_accept_~s.base_12))) + (let ((?x1032 (select |#memory_$Pointer$.base_52| ssl3_accept_~s.base_12))) + (let ((?x1054 (store |#memory_$Pointer$.base_52| ssl3_accept_~s.base_12 (store ?x1032 ?x1050 (select ?x1051 ?x1050))))) + (let (($x1055 (= |#memory_$Pointer$.base_53| ?x1054))) + (let (($x11490 (and $x1055 $x3088))) + (not $x11490)))))))))))) +(assert + (let (($x3458 (>= ssl3_accept_~ret~10_753 |ssl3_accept_#t~nondet159_515|))) + (let (($x2065 (not (<= ssl3_accept_~ret~10_314 0)))) + (let (($x50182 (and $x2065 $x3458))) + (not $x50182))))) +(assert + (let (($x2542 (not (= |ssl3_accept_#t~mem22_459| 16384)))) + (let ((?x1068 (+ ssl3_accept_~s.offset_12 |#offset~STRUCT#?version~INT?type~INT?method~$Pointer$?rbio~$Pointer$?wbio~$Pointer$?bbio~$Pointer$?rwstate~INT?in_handshake~INT?handshake_func~$Pointer$?server~INT?new_session~INT?quiet_shutdown~INT?shutdown~INT?state~INT?rstate~INT?init_buf~$Pointer$?init_num~INT?init_off~INT?packet~$Pointer$?packet_length~UINT?s2~$Pointer$?s3~$Pointer$?read_ahead~INT?hit~INT?purpose~INT?trust~INT?cipher_list~$Pointer$?cipher_list_by_id~$Pointer$?enc_read_ctx~$Pointer$?read_hash~$Pointer$?expand~$Pointer$?enc_write_ctx~$Pointer$?write_hash~$Pointer$?compress~$Pointer$?cert~$Pointer$?sid_ctx_length~UINT?sid_ctx~ARRAY#_32_~UCHAR#?session~$Pointer$?verify_mode~INT?verify_depth~INT?verify_callback~$Pointer$?info_callback~$Pointer$?error~INT?error_code~INT?ctx~$Pointer$?debug~INT?verify_result~LONG?ex_data~~CRYPTO_EX_DATA?client_CA~$Pointer$?references~INT?options~ULONG?mode~ULONG?first_packet~INT?client_version~INT#~s3|))) + (let ((?x2719 (select |#memory_$Pointer$.offset_521| ssl3_accept_~s.base_12))) + (let ((?x2734 (select ?x2719 ?x1068))) + (let (($x2925 (<= |ssl3_accept_#t~mem165.offset_593| ?x2734))) + (and $x2925 $x2542))))))) +(assert + (let (($x2547 (not (= |ssl3_accept_#t~mem23_461| 8192)))) + (let (($x73 (= |#offset~STRUCT#?version~INT?type~INT?method~$Pointer$?rbio~$Pointer$?wbio~$Pointer$?bbio~$Pointer$?rwstate~INT?in_handshake~INT?handshake_func~$Pointer$?server~INT?new_session~INT?quiet_shutdown~INT?shutdown~INT?state~INT?rstate~INT?init_buf~$Pointer$?init_num~INT?init_off~INT?packet~$Pointer$?packet_length~UINT?s2~$Pointer$?s3~$Pointer$?read_ahead~INT?hit~INT?purpose~INT?trust~INT?cipher_list~$Pointer$?cipher_list_by_id~$Pointer$?enc_read_ctx~$Pointer$?read_hash~$Pointer$?expand~$Pointer$?enc_write_ctx~$Pointer$?write_hash~$Pointer$?compress~$Pointer$?cert~$Pointer$?sid_ctx_length~UINT?sid_ctx~ARRAY#_32_~UCHAR#?session~$Pointer$?verify_mode~INT?verify_depth~INT?verify_callback~$Pointer$?info_callback~$Pointer$?error~INT?error_code~INT?ctx~$Pointer$?debug~INT?verify_result~LONG?ex_data~~CRYPTO_EX_DATA?client_CA~$Pointer$?references~INT?options~ULONG?mode~ULONG?first_packet~INT?client_version~INT#~packet| 72))) + (let (($x11452 (and $x73 $x2547))) + (not $x11452))))) +(check-sat) |