Hi,
For bug1.smt2, bug2.smt2, bug3.smt2:
[653] % z3 smt.string_solver=z3str3 bug1.smt2
Segmentation fault
[654] % z3 smt.string_solver=z3str3 model_validate=true bug1.smt2
sat
[655] %
[655] % z3 smt.string_solver=z3str3 bug2.smt2
sat
[656] % z3 smt.string_solver=z3str3 model_validate=true bug2.smt2
Segmentation fault
[657] %
[657] % z3 smt.string_solver=z3str3 bug3.smt2
Segmentation fault
[658] % z3 smt.string_solver=z3str3 model_validate=true bug3.smt2
Segmentation fault
[659] %
[659] % cat bug1.smt2
(declare-fun s () String)
(assert (distinct s "<a></a>"))
(assert (< (str.indexof s "<a>" 16) (str.indexof s "</a>" 23)))
(check-sat)
[660] % cat bug2.smt2
(declare-fun s () String)
(assert (distinct s "<a></a>"))
(assert (< (str.indexof s "<a>" 8) (str.indexof s "</a>" 13)))
(check-sat)
[661] % cat bug3.smt2
(declare-fun s () String)
(assert (distinct s "<a></a>"))
(assert (< (str.indexof s "<a>" 4) (str.indexof s "</a>" 7)))
(check-sat)
These three formulas only have difference on constants, but trigger different segmenation fault behavior.
bug1 triggers z3str3 segmentation fault but z3str3 can give sat with model validation.
bug2 triggers z3str3 with model validation segmenation fault but without validation z3str3 gives sat.
bug3 triggers both z3str3 with and without model validation throws out segmentation faults.
OS: Ubuntu 18.04
Commit: 1119961
Hi,
For bug1.smt2, bug2.smt2, bug3.smt2:
These three formulas only have difference on constants, but trigger different segmenation fault behavior.
bug1 triggers z3str3 segmentation fault but z3str3 can give sat with model validation.
bug2 triggers z3str3 with model validation segmenation fault but without validation z3str3 gives sat.
bug3 triggers both z3str3 with and without model validation throws out segmentation faults.
OS: Ubuntu 18.04
Commit: 1119961