Hi,
For this formula:
(set-logic ALL)
(declare-fun a () String)
(declare-fun b () Int)
(assert
(=
(str.replace "" (int.to.str b) a)
(str.++
(str.replace (str.substr a b 1) (str.substr a b 7) "")
(str.substr a (+ b 1) (str.len a)))))
(check-sat)
Z3 smt.arith.solver=3 throws out an assertion violation:
(smt.diff_logic: non-diff logic expression (+ (- 1) (str.len a) (* (- 1) b)))
ASSERTION VIOLATION
File: ../src/util/old_vector.h
Line: 370
idx < size()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
If we change 7 to 1:
(set-logic ALL)
(declare-fun a () String)
(declare-fun b () Int)
(assert
(=
(str.replace "" (int.to.str b) a)
(str.++
(str.replace (str.substr a b 1) (str.substr a b 1) "")
(str.substr a (+ b 1) (str.len a)))))
(check-sat)
Z3 smt.arith.solver=3 throws out a segmentation fault.
OS: Ubuntu 18.04
Revision: 17d67c1
Hi,
For this formula:
Z3 smt.arith.solver=3 throws out an assertion violation:
If we change
7to1:Z3 smt.arith.solver=3 throws out a segmentation fault.
OS: Ubuntu 18.04
Revision: 17d67c1