z3 icon indicating copy to clipboard operation
z3 copied to clipboard

Published 20 hours ago • verified publisher icon Z3Prover

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

Open iwob opened this issue 7 years ago • 5 comments

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

iwob avatar Nov 27 '17 23:11 iwob

This is for @mtrberzi

NikolajBjorner avatar Nov 27 '17 23:11 NikolajBjorner

I will investigate this.

mtrberzi avatar Nov 29 '17 22:11 mtrberzi

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

mtrberzi avatar Nov 29 '17 23:11 mtrberzi

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

mtrberzi avatar Dec 03 '17 00:12 mtrberzi

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

mtrberzi avatar Apr 26 '20 20:04 mtrberzi