Iwo Błądek

icon indicating a website link https://www.cs.put.poznan.pl/ibladek/ icon indicating an email [email protected]

icon company Poznan University of Technology icon location Poznan. Poland

Results 2 issues of Iwo Błądek

[String] Different satisfiability result with and without smt.string_solver=z3str3

5 comment

Tested on HEAD (81ec5bae9500756bd7ea28a1da28afcdb0ca848f). The following [file](https://github.com/Z3Prover/z3/files/1507923/str5.txt) produces either sat or unsat depending on whether z3str3 was used. Expected is sat.

z3str3

[String] A difficult problem or a bug

8 comment

Hello, this file: [tmp8.txt](https://github.com/Z3Prover/z3/files/1503935/tmp8.txt) is very hard for the solver and it seems to run indefinitely. Is this perhaps a bug? A human can immediately find a counterexample for such...

z3str3