search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.26k stars 1.48k forks source link

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

Open iwob opened 6 years ago

iwob commented 6 years ago

Tested on HEAD (81ec5bae9500756bd7ea28a1da28afcdb0ca848f). The following file produces either sat or unsat depending on whether z3str3 was used. Expected is sat.

NikolajBjorner commented 6 years ago

This is for @mtrberzi

mtrberzi commented 6 years ago

I will investigate this.

mtrberzi commented 6 years ago

I've identified the issue and will open a PR once I have run tests on my end.

mtrberzi commented 6 years ago

Opened #1385. This at least fixes the incorrect solution; I'll work on the performance of this encoding next.

mtrberzi commented 4 years ago

I have a fix in progress for this, and it will be opened as a pull request soon.