Solution soundness on QF_S formula

[wintered]

Commit: bf692a5

The following trace shows a solution unsoundness in QF_S formula. Unfortunately, the formula couldn't be reduced any further. Dropping asserts leads z3 to return unsat.

z3release delta.out.smt2
sat
z3release proof=true delta.out.smt2
unsat
(declare-fun sigmaStar_safe_50 () String)
(declare-fun b_sigmaStar_safe_50 () Bool)
(declare-fun sigmaStar_safe_51 () String)
(declare-fun b_sigmaStar_safe_51 () Bool)
(declare-fun literal_10 () String)
(declare-fun b_literal_10 () Bool)
(declare-fun sigmaStar_055 () String)
(declare-fun b_sigmaStar_055 () Bool)
(declare-fun literal_22 () String)
(declare-fun b_literal_22 () Bool)
(declare-fun literal_25 () String)
(declare-fun b_literal_25 () Bool)
(declare-fun literal_33 () String)
(declare-fun b_literal_33 () Bool)
(declare-fun literal_32 () String)
(declare-fun b_literal_32 () Bool)
(declare-fun literal_31 () String)
(declare-fun b_literal_31 () Bool)
(declare-fun literal_30 () String)
(declare-fun b_literal_30 () Bool)
(declare-fun literal_29 () String)
(declare-fun b_literal_29 () Bool)
(declare-fun literal_39 () String)
(declare-fun b_literal_39 () Bool)
(declare-fun literal_40 () String)
(declare-fun b_literal_40 () Bool)
(declare-fun literal_50 () String)
(declare-fun b_literal_50 () Bool)
(declare-fun literal_56 () String)
(declare-fun b_literal_56 () Bool)
(declare-fun literal_62 () String)
(declare-fun b_literal_62 () Bool)
(declare-fun literal_61 () String)
(declare-fun b_literal_61 () Bool)
(declare-fun literal_60 () String)
(declare-fun b_literal_60 () Bool)
(declare-fun literal_59 () String)
(declare-fun b_literal_59 () Bool)
(declare-fun literal_58 () String)
(declare-fun b_literal_58 () Bool)
(declare-fun literal_63 () String)
(declare-fun b_literal_63 () Bool)
(declare-fun atkPtn () String)
(declare-fun x_9 () String)
(declare-fun b_x_9 () Bool)
(declare-fun x_13 () String)
(declare-fun b_x_13 () Bool)
(declare-fun x_14 () String)
(declare-fun b_x_14 () Bool)
(declare-fun x_20 () String)
(declare-fun b_x_20 () Bool)
(declare-fun x_23 () String)
(declare-fun b_x_23 () Bool)
(declare-fun x_28 () String)
(declare-fun b_x_28 () Bool)
(declare-fun x_35 () String)
(declare-fun b_x_35 () Bool)
(declare-fun x_36 () String)
(declare-fun b_x_36 () Bool)
(declare-fun x_37 () String)
(declare-fun b_x_37 () Bool)
(declare-fun x_38 () String)
(declare-fun b_x_38 () Bool)
(declare-fun x_44 () String)
(declare-fun b_x_44 () Bool)
(declare-fun x_45 () String)
(declare-fun b_x_45 () Bool)
(declare-fun x_51 () String)
(declare-fun b_x_51 () Bool)
(declare-fun x_54 () String)
(declare-fun b_x_54 () Bool)
(declare-fun x_55 () String)
(declare-fun b_x_55 () Bool)
(declare-fun x_57 () String)
(declare-fun b_x_57 () Bool)
(declare-fun x_64 () String)
(declare-fun b_x_64 () Bool)
(declare-fun x_65 () String)
(declare-fun b_x_65 () Bool)
(declare-fun x_66 () String)
(declare-fun b_x_66 () Bool)
(declare-fun x_67 () String)
(declare-fun b_x_67 () Bool)
(declare-fun x_68 () String)
(declare-fun b_x_68 () Bool)
(declare-fun x_69 () String)
(declare-fun b_x_69 () Bool)
(declare-fun x_70 () String)
(declare-fun b_x_70 () Bool)
(declare-fun sink () String)
(declare-fun atk_sigmaStar_1 () String)
(declare-fun atk_sigmaStar_2 () String)
(declare-fun atk_sink () String)
(assert (= b_sigmaStar_safe_50 (str.in_re sigmaStar_safe_50 (re.* (re.union (re.range "0" "9") (re.union (re.range "a" "z") (re.range (str.from_code (+ (str.len x_68) (str.len sink))) "Z")))))))
(assert (and b_literal_33 (= literal_33 "\u\u\u")))
(assert (and b_literal_32 (= literal_32 "\u\u\u")))
(assert (and (= literal_31 "\u\u\u")))
(assert (and b_literal_30 (= literal_30 "\u\u\u")))
(assert (and b_literal_29 (= literal_29 "\u\u\u")))
(assert (and b_literal_39 (= literal_39 "\u{53}\u{45}\u{4c}\u{45}\u{43}\u{54}\u{20}\u{43}\u{6f}\u{75}\u{6e}\u{74}")))
(assert (and b_literal_50 (= literal_50 "\u{20}\u{46}\u{52}\u{4f}\u{4d}\u{20}")))
(assert (and b_literal_56 (= literal_56 "\u{20}\u{57}\u{48}\u{45}\u{52}\u{45}\u{20}")))
(assert (and b_literal_62 (= literal_62 "\u{61}\u{64}\u{6d}\u{69}\u{6e}")))
(assert (and b_literal_61 (= literal_61 "\u{62}\u{6c}\u{61}\u{63}\u{6b}\u{6c}\u{69}\u{73}\u{74}")))
(assert (and b_literal_60 (= literal_60 "\u{61}\u{64}\u{6d}\u{69}\u{6e}")))
(assert (and b_literal_59 (= literal_59 "\u{61}\u{64}\u{6d}\u{69}\u{6e}")))
(assert (and b_literal_58 (= literal_58 "\u{61}\u{64}\u{6d}\u{69}\u{6e}")))
(assert (and b_literal_63 (= literal_63 "")))
(assert (str.in_re atkPtn (str.to_re "' or 1=1 '")))
(assert (= atk_sink (str.++ atk_sigmaStar_1 (str.++ atkPtn atk_sigmaStar_2))))
(assert (= b_x_9 (or (and (= x_9 sigmaStar_safe_50) b_sigmaStar_safe_50) (and (= x_9 sigmaStar_safe_51) b_sigmaStar_safe_51))))
(assert (= b_x_13 (or (and (= x_13 x_9) b_x_9) (and (= x_13 literal_10) b_literal_10))))
(assert (= b_x_14 (or (and (= x_14 x_13) b_x_13) (and (= x_14 sigmaStar_055) b_sigmaStar_055))))
(assert (= b_x_20 (and (= x_20 (str.replace x_14 "." "' OR admin_rights='")) b_x_14)))
(assert (= b_x_23 (and (= x_23 (str.++ literal_22 x_20)) b_literal_22 b_x_20)))
(assert (= b_x_28 (and (= x_28 (str.++ x_23 literal_25)) b_x_23 b_literal_25)))
(assert (= b_x_35 (or (and (= x_35 literal_33) b_literal_33) (and (= x_35 literal_32) b_literal_32))))
(assert (= b_x_36 (or (and (= x_36 x_35) b_x_35) (and (= x_36 literal_31) b_literal_31))))
(assert (= b_x_37 (or (and (= x_37 x_36) b_x_36) (and (= x_37 literal_30) b_literal_30))))
(assert (= b_x_38 (or (and (= x_38 x_37) b_x_37) (and (= x_38 literal_29) b_literal_29))))
(assert (= b_x_44 (and (= x_44 (str.++ literal_39 x_38)) b_literal_39 b_x_38)))
(assert (= b_x_45 (and (= x_45 (str.++ x_28 literal_40)) b_x_28 b_literal_40)))
(assert (= b_x_51 (and (= x_51 (str.++ x_44 literal_50)) b_x_44 b_literal_50)))
(assert (= b_x_55 (or (and (= x_55 x_54) b_x_54) (and (= x_55 x_45) b_x_45))))
(assert (= b_x_57 (and (= x_57 (str.++ literal_56 x_55)) b_literal_56 b_x_55)))
(assert (= b_x_64 (or (and (= x_64 literal_62) b_literal_62) (and (= x_64 literal_61) b_literal_61))))
(assert (= b_x_65 (or (and (= x_65 x_64) b_x_64) (and (= x_65 literal_60) b_literal_60))))
(assert (= b_x_66 (or (and (= x_66 x_65) b_x_65) (and (= x_66 literal_59) b_literal_59))))
(assert (= b_x_67 (or (and (= x_67 x_66) b_x_66) (and (= x_67 literal_58) b_literal_58))))
(assert (= b_x_68 (or (and (= x_68 literal_63) b_literal_63) (and (= x_68 x_57) b_x_57))))
(assert (= b_x_69 (and (= x_69 (str.++ x_51 x_67)) b_x_51 b_x_67)))
(assert (= b_x_70 (and (= x_70 (str.++ x_69 x_68)) b_x_69 b_x_68)))
(assert (and (= sink x_70) (= sink atk_sink) b_x_70))
(assert (> 50 (+ (str.len x_68) (str.len sink))))
(check-sat)