Skip to content

Z3str3 segmentation fault on String formula with distinct, str.indexof, str.contains, str.len #2743

@muchang

Description

@muchang

Hi,
For this formula,

(declare-fun string () String)
(assert
 (and
  (and
   (and (or (and (distinct (ite (> (str.indexof string ";" 239) 57) 207 202) 202))))
   (and (distinct (ite (or (distinct (str.len string) 244)) 57 193) 182)))
  (or (or (distinct (ite (str.contains string "") 218 68) 87)))))
(check-sat)

Z3str3 thorws out a segmentation fault while solving this formula.

OS: Ubuntu 18.04
Revision: 5f78ca9

Metadata

Metadata

Assignees

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions