(z3str3, rewriter.arith_ineq_lhs, smt.str.fixed_length_naive_cex=false, dom-simplify, ctx-solver-simplify) Assertion violation at ../src/ast/ast.h Line: 492 or 431

[muchang]

Hi,
For this formula, Z3 throws out an assertion violation:

[617] % z3release smt.string_solver=z3str3 small.smt2
ASSERTION VIOLATION
File: ../src/ast/ast.cpp
Line: 431
UNREACHABLE CODE WAS REACHED.
Z3 4.8.9.0
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new
[618] % 
[618] % z3debug smt.string_solver=z3str3 small.smt2
ASSERTION VIOLATION
File: ../src/ast/ast.h
Line: 492
m_ref_count > 0
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[619] % 
[619] % cat small.smt2
(set-option :rewriter.arith_ineq_lhs true)
(set-option :smt.str.fixed_length_naive_cex false)
(declare-fun a () Bool)
(declare-fun b () Bool)
(declare-fun c () Bool)
(declare-fun d () String)
(declare-fun e () String)
(declare-fun f () Bool)
(declare-fun g () String)
(declare-fun h () Bool)
(declare-fun i () Bool)
(declare-fun j () Bool)
(declare-fun aa () Bool)
(assert (not (= "" (str.substr d 0 (str.len e)))))
(assert (= i (= "-" (str.substr d 0 (str.len e)))))
(assert (= (= b f) (= "-" e)))
(assert (= j (= b c)))
(assert (= aa (= "" (str.substr d 0 (str.len e)))))
(assert (= a (= h f)))
(assert b)
(assert (= d (str.++ e g)))
(check-sat-using (then dom-simplify ctx-solver-simplify))
[620] %

OS: Ubuntu 18.04
Commit: fc8dfe3

[rainoftime]

Another instance at ast.h:492

(set-option :smt.arith.solver 2)
(set-option :smt.str.fixed_length_naive_cex false)
(set-option :smt.string_solver z3str3)
(declare-const Str10 String)
(declare-const Str13 String)
(declare-const Str15 String)
(assert (str.contains Str15 (str.++ Str10 Str13 "gdtkeq" "")))
(check-sat-using (then simplify ctx-solver-simplify unit-subsume-simplify card2bv smt))

[mtrberzi]

Fixed in 04ac5f0