Hi,
For the following logic Z3 with --smt.string_solver=z3str3 gives an assertion violation
(set-logic QF_S)
(declare-fun a () String)
(assert (= (str.indexof (str.++ "x" a) "y" 0) (str.indexof (str.++ a "x") "y" 2)))
(check-sat)
ASSERTION VIOLATION
File: ../src/util/rational.h
Line: 113
is_unsigned()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
OS: Ubuntu 18.04
Revision: d95b549
Hi,
For the following logic Z3 with
--smt.string_solver=z3str3gives an assertion violationOS: Ubuntu 18.04
Revision: d95b549