Assertion violation at smt_conflict_resolution.cpp:1082 (z3str3, proof, smt.arith.eager_eq_axioms, smt.arith.solver, smt.phase_selection)

[rainoftime]

(set-option :proof true)
(set-option :smt.arith.eager_eq_axioms false)
(set-option :smt.arith.solver 2)
(set-option :smt.phase_selection 1)
(set-option :smt.string_solver z3str3)
(declare-const i2 Int)
(declare-const i5 Int)
(declare-const Str1 String)
(declare-const Str4 String)
(declare-const Str11 String)
(declare-const Str13 String)
(declare-const Str14 String)
(declare-const Str15 String)
(declare-const Str18 String)
(declare-const Str19 String)
(assert (>= (str.len Str19) 238))
(declare-const v19 Bool)
(check-sat)
(check-sat-assuming ((! (or (= (<= 0 3 238 (+ 6 73 74 89)) true (not true) true (not true) true true) v19 (distinct (str.++ Str4 Str13) "lpyrqe")) :named IP_14) (! (or (or (distinct (str.++ Str4 Str13) "lpyrqe") (and true true true (> 854 6) (>= i2 (abs i5) (mod i5 i2) 244) true true (or true true) (> 854 6) true) (not true)) (or (and true true true (> 854 6) (>= i2 (abs i5) (mod i5 i2) 244) true true (or true true) (> 854 6) true) (not true) (str.suffixof Str1 ""))) :named IP_27)))
(check-sat-assuming ((! (or (and true true true (> 854 6) (>= i2 (abs i5) (mod i5 i2) 244) true true (or true true) (> 854 6) true) (not true) (str.suffixof Str1 "")) :named IP_2) (! (=> (or (distinct (str.++ Str4 Str14) (str.++ "" "") (str.++ (str.++ Str13 Str11 "" Str13) (int.to.str 854)) (str.++ Str4 Str14)) v19 (not true)) (or (or (distinct (str.++ Str4 Str14) (str.++ "" "") (str.++ (str.++ Str13 Str11 "" Str13) (int.to.str 854)) (str.++ Str4 Str14)) (not true) (and true true (distinct Str1 "" "" "" "") true (or true true) (<= 0 (abs i5)) (xor true true true true true (not true) true) true)) (or (and true (= true true true true) (<= (- 0) 6) (< i5 (abs 244)) (not (distinct Str15 Str19 Str18)) (= (<= 0 3 238 (+ 6 73 74 89)) true (not true) true (not true) true true)) v19 (str.suffixof Str1 "")))) :named IP_26)))
(check-sat-assuming ((! (=> (or (and true true (distinct Str1 "" "" "" "") true (or true true) (<= 0 (abs i5)) (xor true true true true true (not true) true) true) (and true true (distinct Str1 "" "" "" "") true (or true true) (<= 0 (abs i5)) (xor true true true true true (not true) true) true) (and true (= true true true true) (<= (- 0) 6) (< i5 (abs 244)) (not (distinct Str15 Str19 Str18)) (= (<= 0 3 238 (+ 6 73 74 89)) true (not true) true (not true) true true))) (or (and true true (distinct Str1 "" "" "" "") true (or true true) (<= 0 (abs i5)) (xor true true true true true (not true) true) true) (and true (= true true true true) (<= (- 0) 6) (< i5 (abs 244)) (not (distinct Str15 Str19 Str18)) (= (<= 0 3 238 (+ 6 73 74 89)) true (not true) true (not true) true true)) (not true))) :named IP_23) (! (or (or (distinct (str.++ Str4 Str13) "lpyrqe") (= (<= 0 3 238 (+ 6 73 74 89)) true (not true) true (not true) true true) (and true true (distinct Str1 "" "" "" "") true (or true true) (<= 0 (abs i5)) (xor true true true true true (not true) true) true)) (or (distinct (str.++ Str4 Str14) (str.++ "" "") (str.++ (str.++ Str13 Str11 "" Str13) (int.to.str 854)) (str.++ Str4 Str14)) v19 (not true))) :named IP_24)))

z3 (commit b2bfb1f)

sat
ASSERTION VIOLATION
File: ../src/smt/smt_conflict_resolution.cpp
Line: 1082
js.get_kind() != b_justification::BIN_CLAUSE
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB