memcpy.smt2

(declare-fun S0_len (Int Int) (_ BitVec 64)); theory len
(declare-fun S1___array__main__SIZE (Int) (_ BitVec 64)); local ::array::main::SIZE
; line 11
; literal expr
(declare-fun S2_literal_3 (Int) (_ BitVec 64)); local literal 3
(assert (= (S2_literal_3 0) (_ bv3 64)))
(assert (= (S1___array__main__SIZE 1)  (S2_literal_3 0)))
(declare-fun S4_boh (Int) (_ BitVec 8)); local boh
; line 14
; call
(declare-fun S5_interpretation_of_theory_len (Int) (_ BitVec 64)); local interpretation of theory len
(assert (= (S0_len 4 0) (S5_interpretation_of_theory_len 0)))
(declare-fun S6_infix_expression (Int) bool); local infix expression
(assert (=  (S6_infix_expression 0)  (= (S5_interpretation_of_theory_len 0) (S1___array__main__SIZE 1))))
; constrain. we know this to be true because of an if condition or callsite assert
(assert (S6_infix_expression 0))
; line 16
; literal expr
(declare-fun S7_literal_2 (Int) (_ BitVec 64)); local literal 2
(assert (= (S7_literal_2 0) (_ bv2 64)))
; begin array bounds
(declare-fun S8_len_boh_ (Int) (_ BitVec 64)); local len(boh)
(assert (= (S0_len 4 0) (S8_len_boh_ 0)))
(declare-fun S9_literal_2___len_boh_ (Int) bool); local literal 2 < len(boh)
(assert (=  (S9_literal_2___len_boh_ 0) (bvult (S7_literal_2 0) (S8_len_boh_ 0))        ))
; assert that length less than index is true
(echo "")
(push)
(echo "vvv positive assert")
(assert (S9_literal_2___len_boh_ 0))
(check-sat)
(pop)
(push)
(echo "vvv negative assert. to be constrained, this must be different")
(assert (not (S9_literal_2___len_boh_ 0)))
(check-sat)
(echo "constrained true")
(pop)
(push)
(assert (S9_literal_2___len_boh_ 0))
(check-sat)
(pop)
(declare-fun S10_array_access (Int) (_ BitVec 8)); local array access
; literal expr
(declare-fun S11_literal_3 (Int) (_ BitVec 64)); local literal 3
(assert (= (S11_literal_3 0) (_ bv3 64)))
(declare-fun S12_literal_3 (Int) (_ BitVec 8)); local literal 3
(assert (= (S12_literal_3 0) (_ bv3 8)))
(assert (= (S10_array_access 1)  (S12_literal_3 0)))
(declare-fun S14_dst (Int) (_ BitVec 8)); local dst
(declare-fun S15_src (Int) (_ BitVec 8)); local src
(declare-fun S16_l (Int) (_ BitVec 64)); local l
; line 2
; literal expr
(declare-fun S17_literal_0 (Int) (_ BitVec 64)); local literal 0
(assert (= (S17_literal_0 0) (_ bv0 64)))
(declare-fun S18_literal_0 (Int) (_ BitVec 64)); local literal 0
(assert (= (S18_literal_0 0) (_ bv0 64)))
(declare-fun S19_infix_expression (Int) bool); local infix expression
(assert (=  (S19_infix_expression 0) (bvugt (S16_l 0) (S18_literal_0 0))        ))
; call
(declare-fun S20_interpretation_of_theory_len (Int) (_ BitVec 64)); local interpretation of theory len
(assert (= (S0_len 14 0) (S20_interpretation_of_theory_len 0)))
(declare-fun S21_infix_expression (Int) bool); local infix expression
(assert (=  (S21_infix_expression 0) (bvuge (S20_interpretation_of_theory_len 0) (S16_l 0))        ))
(declare-fun S22_infix_expression (Int) bool); local infix expression
(assert (=  (S22_infix_expression 0) (and (S19_infix_expression 0) (S21_infix_expression 0))        ))
; call
(declare-fun S23_interpretation_of_theory_len (Int) (_ BitVec 64)); local interpretation of theory len
(assert (= (S0_len 15 0) (S23_interpretation_of_theory_len 0)))
(declare-fun S24_infix_expression (Int) bool); local infix expression
(assert (=  (S24_infix_expression 0) (bvuge (S23_interpretation_of_theory_len 0) (S16_l 0))        ))
(declare-fun S25_infix_expression (Int) bool); local infix expression
(assert (=  (S25_infix_expression 0) (and (S22_infix_expression 0) (S24_infix_expression 0))        ))
; constrain. we know this to be true because of an if condition or callsite assert
(assert (S25_infix_expression 0))
(push); for loop
(declare-fun S26_i (Int) (_ BitVec 64)); local i
; line 4
; literal expr
(declare-fun S27_literal_0 (Int) (_ BitVec 64)); local literal 0
(assert (= (S27_literal_0 0) (_ bv0 64)))
(assert (= (S26_i 1)  (S27_literal_0 0)))
(declare-fun S28_previous_value_of_i (Int) (_ BitVec 64)); local previous value of i
(declare-fun S29_infix_expression (Int) bool); local infix expression
(assert (=  (S29_infix_expression 0) (bvult (S26_i 2) (S16_l 0))        ))
; constrain. we know this to be true because of an if condition or callsite assert
(assert (S29_infix_expression 0))
; line 5
; begin array bounds
(declare-fun S30_len_dst_ (Int) (_ BitVec 64)); local len(dst)
(assert (= (S0_len 14 0) (S30_len_dst_ 0)))
(declare-fun S31_i___len_dst_ (Int) bool); local i < len(dst)
(assert (=  (S31_i___len_dst_ 0) (bvult (S26_i 2) (S30_len_dst_ 0))        ))
; assert that length less than index is true
(echo "")
(push)
(echo "vvv positive assert")
(assert (S31_i___len_dst_ 0))
(check-sat)
(pop)
(push)
(echo "vvv negative assert. to be constrained, this must be different")
(assert (not (S31_i___len_dst_ 0)))
(check-sat)
(echo "constrained true")
(pop)
(push)
(assert (S31_i___len_dst_ 0))
(check-sat)
(pop)
(declare-fun S32_array_access (Int) (_ BitVec 8)); local array access
; begin array bounds
(declare-fun S33_len_src_ (Int) (_ BitVec 64)); local len(src)
(assert (= (S0_len 15 0) (S33_len_src_ 0)))
(declare-fun S34_i___len_src_ (Int) bool); local i < len(src)
(assert (=  (S34_i___len_src_ 0) (bvult (S26_i 2) (S33_len_src_ 0))        ))
; assert that length less than index is true
(echo "")
(push)
(echo "vvv positive assert")
(assert (S34_i___len_src_ 0))
(check-sat)
(pop)
(push)
(echo "vvv negative assert. to be constrained, this must be different")
(assert (not (S34_i___len_src_ 0)))
(check-sat)
(echo "constrained true")
(pop)
(push)
(assert (S34_i___len_src_ 0))
(check-sat)
(pop)
(declare-fun S35_array_access (Int) (_ BitVec 8)); local array access
(assert (= (S32_array_access 1)  (S35_array_access 0)))
(pop); end of for loop
(declare-fun S37_src (Int) (_ BitVec 8)); local src
; line 20
; literal expr
(declare-fun S38_literal_23 (Int) (_ BitVec 64)); local literal 23
(assert (= (S38_literal_23 0) (_ bv23 64)))
(push)
(check-sat)
(get-value (S38_literal_23 0))
(pop)
;  = #x0000000000000017
(push)
(assert (not (= (_ bv23 64) (S38_literal_23 0))))
(check-sat)
(get-value (S38_literal_23 0))
(pop)
(declare-fun S39_len_src_ (Int) (_ BitVec 64)); local len(src)
(assert (= (S0_len 37 0) (S39_len_src_ 0)))
(assert (= (S39_len_src_ 0) (_ bv23 64)))
(declare-fun S40_literal_array_40 (Int) (_ BitVec 64)); local literal array 40
(declare-fun S41_literal_array_41 (Int) (_ BitVec 64)); local literal array 41
; literal expr
(declare-fun S42_literal_0 (Int) (_ BitVec 64)); local literal 0
(assert (= (S42_literal_0 0) (_ bv0 64)))
(declare-fun S43_literal_array_init_41_0_43 (Int) (_ BitVec 64)); local literal array init 41 0 43
(declare-fun S44_len_src_ (Int) (_ BitVec 64)); local len(src)
(assert (= (S0_len 37 1) (S44_len_src_ 0)))
(assert (= (S44_len_src_ 0) (_ bv23 64)))
(declare-fun S45_f (Int) (_ BitVec 8)); local f
; line 21
(push)
(check-sat)
(get-value (S1___array__main__SIZE 1))
(pop)
;  = #x0000000000000003
(push)
(assert (not (= (_ bv3 64) (S1___array__main__SIZE 1))))
(check-sat)
(get-value (S1___array__main__SIZE 1))
(pop)
(declare-fun S46_len_f_ (Int) (_ BitVec 64)); local len(f)
(assert (= (S0_len 45 0) (S46_len_f_ 0)))
(assert (= (S46_len_f_ 0) (_ bv3 64)))
(declare-fun S47_literal_array_47 (Int) (_ BitVec 64)); local literal array 47
(declare-fun S48_literal_array_48 (Int) (_ BitVec 64)); local literal array 48
; literal expr
(declare-fun S49_literal_0 (Int) (_ BitVec 64)); local literal 0
(assert (= (S49_literal_0 0) (_ bv0 64)))
(declare-fun S50_literal_array_init_48_0_50 (Int) (_ BitVec 64)); local literal array init 48 0 50
(declare-fun S51_len_f_ (Int) (_ BitVec 64)); local len(f)
(assert (= (S0_len 45 1) (S51_len_f_ 0)))
(assert (= (S51_len_f_ 0) (_ bv3 64)))
; line 23
; call
(push); callsite_assert
(declare-fun S52_dst (Int) (_ BitVec 8)); local dst
(declare-fun S53_len_dst_ (Int) (_ BitVec 64)); local len(dst)
(assert (= (S0_len 52 1) (S53_len_dst_ 0)))
(assert (= (S53_len_dst_ 0) (_ bv3 64)))
(assert (= (S52_dst 1)  (S45_f 1)))
(declare-fun S54_src (Int) (_ BitVec 8)); local src
(declare-fun S55_len_src_ (Int) (_ BitVec 64)); local len(src)
(assert (= (S0_len 54 1) (S55_len_src_ 0)))
(assert (= (S55_len_src_ 0) (_ bv23 64)))
(assert (= (S54_src 1)  (S37_src 1)))
(declare-fun S56_l (Int) (_ BitVec 64)); local l
(assert (= (S56_l 1)  (S1___array__main__SIZE 1)))
; line 2
; literal expr
(declare-fun S57_literal_0 (Int) (_ BitVec 64)); local literal 0
(assert (= (S57_literal_0 0) (_ bv0 64)))
(declare-fun S58_literal_0 (Int) (_ BitVec 64)); local literal 0
(assert (= (S58_literal_0 0) (_ bv0 64)))
(declare-fun S59_infix_expression (Int) bool); local infix expression
(assert (=  (S59_infix_expression 0) (bvugt (S56_l 1) (S58_literal_0 0))        ))
; call
(declare-fun S60_interpretation_of_theory_len (Int) (_ BitVec 64)); local interpretation of theory len
(assert (= (S0_len 52 1) (S60_interpretation_of_theory_len 0)))
(declare-fun S61_infix_expression (Int) bool); local infix expression
(assert (=  (S61_infix_expression 0) (bvuge (S60_interpretation_of_theory_len 0) (S56_l 1))        ))
(declare-fun S62_infix_expression (Int) bool); local infix expression
(assert (=  (S62_infix_expression 0) (and (S59_infix_expression 0) (S61_infix_expression 0))        ))
; call
(declare-fun S63_interpretation_of_theory_len (Int) (_ BitVec 64)); local interpretation of theory len
(assert (= (S0_len 54 1) (S63_interpretation_of_theory_len 0)))
(declare-fun S64_infix_expression (Int) bool); local infix expression
(assert (=  (S64_infix_expression 0) (bvuge (S63_interpretation_of_theory_len 0) (S56_l 1))        ))
(declare-fun S65_infix_expression (Int) bool); local infix expression
(assert (=  (S65_infix_expression 0) (and (S62_infix_expression 0) (S64_infix_expression 0))        ))
(echo "")
(push)
(echo "vvv positive assert")
(assert (S65_infix_expression 0))
(check-sat)
(pop)
(push)
(echo "vvv negative assert. to be constrained, this must be different")
(assert (not (S65_infix_expression 0)))
(check-sat)
(echo "constrained true")
(pop)
(push)
(assert (S65_infix_expression 0))
(check-sat)
(pop)
(pop); end of callsite_assert
; line 26
; literal expr
(declare-fun S67_literal_1 (Int) (_ BitVec 64)); local literal 1
(assert (= (S67_literal_1 0) (_ bv1 64)))
(push)
(check-sat)
(get-value (S67_literal_1 0))
(pop)
;  = #x0000000000000001
(push)
(assert (not (= (_ bv1 64) (S67_literal_1 0))))
(check-sat)
(get-value (S67_literal_1 0))
(pop)
; begin array bounds
(declare-fun S68_len_src_ (Int) (_ BitVec 64)); local len(src)
(assert (= (S0_len 37 1) (S68_len_src_ 0)))
(declare-fun S69_literal_1___len_src_ (Int) bool); local literal 1 < len(src)
(assert (=  (S69_literal_1___len_src_ 0) (bvult (S67_literal_1 0) (S68_len_src_ 0))        ))
; assert that length less than index is true
(echo "")
(push)
(echo "vvv positive assert")
(assert (S69_literal_1___len_src_ 0))
(check-sat)
(pop)
(push)
(echo "vvv negative assert. to be constrained, this must be different")
(assert (not (S69_literal_1___len_src_ 0)))
(check-sat)
(echo "constrained true")
(pop)
(push)
(assert (S69_literal_1___len_src_ 0))
(check-sat)
(pop)
(declare-fun S70_array_access (Int) (_ BitVec 8)); local array access
; literal expr
(declare-fun S71_literal_3 (Int) (_ BitVec 64)); local literal 3
(assert (= (S71_literal_3 0) (_ bv3 64)))
(declare-fun S72_literal_3 (Int) (_ BitVec 8)); local literal 3
(assert (= (S72_literal_3 0) (_ bv3 8)))
(assert (= (S70_array_access 1)  (S72_literal_3 0)))
(declare-fun S73_dst (Int) (_ BitVec 8)); local dst
; line 28
; literal expr
(declare-fun S74_literal_20 (Int) (_ BitVec 64)); local literal 20
(assert (= (S74_literal_20 0) (_ bv20 64)))
(push)
(check-sat)
(get-value (S74_literal_20 0))
(pop)
;  = #x0000000000000014
(push)
(assert (not (= (_ bv20 64) (S74_literal_20 0))))
(check-sat)
(get-value (S74_literal_20 0))
(pop)
(declare-fun S75_len_dst_ (Int) (_ BitVec 64)); local len(dst)
(assert (= (S0_len 73 0) (S75_len_dst_ 0)))
(assert (= (S75_len_dst_ 0) (_ bv20 64)))
(declare-fun S76_literal_array_76 (Int) (_ BitVec 64)); local literal array 76
(declare-fun S77_literal_array_77 (Int) (_ BitVec 64)); local literal array 77
; literal expr
(declare-fun S78_literal_0 (Int) (_ BitVec 64)); local literal 0
(assert (= (S78_literal_0 0) (_ bv0 64)))
(declare-fun S79_literal_array_init_77_0_79 (Int) (_ BitVec 64)); local literal array init 77 0 79
(declare-fun S80_len_dst_ (Int) (_ BitVec 64)); local len(dst)
(assert (= (S0_len 73 1) (S80_len_dst_ 0)))
(assert (= (S80_len_dst_ 0) (_ bv20 64)))
; line 29
; call
; call
; call
(declare-fun S81_interpretation_of_theory_len (Int) (_ BitVec 64)); local interpretation of theory len
(assert (= (S0_len 73 1) (S81_interpretation_of_theory_len 0)))
(push)
(check-sat)
(get-value (S81_interpretation_of_theory_len 0))
(pop)
;  = #x0000000000000014
(push)
(assert (not (= (_ bv20 64) (S81_interpretation_of_theory_len 0))))
(check-sat)
(get-value (S81_interpretation_of_theory_len 0))
(pop)
(declare-fun S82_literal_20 (Int) (_ BitVec 64)); local literal 20
(assert (= (S82_literal_20 0) (_ bv20 64)))
(push); callsite_assert
(declare-fun S83_dst (Int) (_ BitVec 8)); local dst
(declare-fun S84_len_dst_ (Int) (_ BitVec 64)); local len(dst)
(assert (= (S0_len 83 1) (S84_len_dst_ 0)))
(assert (= (S84_len_dst_ 0) (_ bv20 64)))
(assert (= (S83_dst 1)  (S73_dst 1)))
(declare-fun S85_src (Int) (_ BitVec 8)); local src
(declare-fun S86_len_src_ (Int) (_ BitVec 64)); local len(src)
(assert (= (S0_len 85 1) (S86_len_src_ 0)))
(assert (= (S86_len_src_ 0) (_ bv23 64)))
(assert (= (S85_src 1)  (S37_src 1)))
(declare-fun S87_l (Int) (_ BitVec 64)); local l
(assert (= (S87_l 1)  (S82_literal_20 0)))
; line 2
; literal expr
(declare-fun S88_literal_0 (Int) (_ BitVec 64)); local literal 0
(assert (= (S88_literal_0 0) (_ bv0 64)))
(declare-fun S89_literal_0 (Int) (_ BitVec 64)); local literal 0
(assert (= (S89_literal_0 0) (_ bv0 64)))
(declare-fun S90_infix_expression (Int) bool); local infix expression
(assert (=  (S90_infix_expression 0) (bvugt (S87_l 1) (S89_literal_0 0))        ))
; call
(declare-fun S91_interpretation_of_theory_len (Int) (_ BitVec 64)); local interpretation of theory len
(assert (= (S0_len 83 1) (S91_interpretation_of_theory_len 0)))
(declare-fun S92_infix_expression (Int) bool); local infix expression
(assert (=  (S92_infix_expression 0) (bvuge (S91_interpretation_of_theory_len 0) (S87_l 1))        ))
(declare-fun S93_infix_expression (Int) bool); local infix expression
(assert (=  (S93_infix_expression 0) (and (S90_infix_expression 0) (S92_infix_expression 0))        ))
; call
(declare-fun S94_interpretation_of_theory_len (Int) (_ BitVec 64)); local interpretation of theory len
(assert (= (S0_len 85 1) (S94_interpretation_of_theory_len 0)))
(declare-fun S95_infix_expression (Int) bool); local infix expression
(assert (=  (S95_infix_expression 0) (bvuge (S94_interpretation_of_theory_len 0) (S87_l 1))        ))
(declare-fun S96_infix_expression (Int) bool); local infix expression
(assert (=  (S96_infix_expression 0) (and (S93_infix_expression 0) (S95_infix_expression 0))        ))
(echo "")
(push)
(echo "vvv positive assert")
(assert (S96_infix_expression 0))
(check-sat)
(pop)
(push)
(echo "vvv negative assert. to be constrained, this must be different")
(assert (not (S96_infix_expression 0)))
(check-sat)
(echo "constrained true")
(pop)
(push)
(assert (S96_infix_expression 0))
(check-sat)
(pop)
(pop); end of callsite_assert