(continuously updating) List of benchmarks on which z3str3 return an incorrect result

[numairmansur]

Hi,
For the following list of benchmarks, z3str3 return incorrect result:

All the files listed below are sat.
z3str3 returns unsat for all of them.
CVC4 returns sat for all of them.
Z3 (without z3str3) retrurns sat for all of them. For some it hangs. Those files are marked with (z3 hangs).

• 1.smt2
• 2.smt2
• 3.smt2
• 4.smt2
• 5.smt2
• 6.smt2
• 7.smt2
• 8.smt2
• 9.smt2 (z3 hangs)
• 10.smt2
• 11.smt2 (z3 hangs)
• 12.smt2 (z3 hangs)
• 13.smt2
• 14.smt2
• 15.smt2
• 16.smt2 (z3 hangs)
• 17.smt2 (z3 hangs)
• 18.smt2
• 19.smt2
• 20.smt2
• 21.smt2
• 22.smt2
• 23.smt2
• 24.smt2
• 25.smt2
• 26.smt2
• 27.smt2
• 28.smt2
• 29.smt2
• 30.smt2
• 31.smt2
• 33.smt2
• 34.smt2
• 35.smt2
• 36.smt2
• 37.smt2
• 38.smt2
• 39.smt2
• 40.smt2
• 41.smt2
• 42.smt2
• 43.smt2

I am using the z3 nightly build
Z3 version 4.8.8 - 64 bit

[NikolajBjorner]

strings4.smt2.zip

[NikolajBjorner]

strings3.smt2.zip

[NikolajBjorner]

strings.smt2.zip

[numairmansur]

Some more examples on the latest nightly build:

44.smt2
45.smt2
46.smt2
47.smt2
48.smt2
49.smt2
50.smt2
51.smt2
52.smt2
53.smt2
54.smt2
55.smt2
56.smt2
57.smt2
58.smt2
59.smt2
60.smt2
61.smt2
62.smt2
63.smt2

[mtrberzi]

Taking a look at these cases. Some are now resolved (z3str3 returns sat), others are actually segfaults and a few are timing out. Is there a way we would prefer to track progress on these (maybe editing the list in the comment)?

[numairmansur]

I can rearrange them.
What timeout are you using ?

[mtrberzi]

20 seconds. I'll post the full list tomorrow (I will need to update the segfaults list as well as I tested those on the latest build).

[mtrberzi]

Actually, what timeout did you use? I could re-test the "timeout" cases if you used a longer interval.

[numairmansur]

The timeout I used was 120 seconds

[mtrberzi]

I re-ran the timeout cases for 120 seconds. Here are the latest results for commit 0b486d26daea05f918643a9d277f12027f0bc2f6 (release build):

Cases which are still UNSAT:

• 28
• 58
• 62

Cases which timeout:

• 2
• 17
• 18
• 23
• 25
• 26
• 27
• 29
• 39
• 41
• 42
• 43
• 44
• 55
• 63
• strings3

Cases which segfault:

• 9
• 10
• 47
• 57

And all 42 other cases return SAT.

[numairmansur]

@mtrberzi Here are some more examples :
15.smt2
13.smt2
12.smt2
11.smt2
10.smt2
9.smt2
8.smt2
7.smt2
6.smt2
3.smt2
2.smt2
1.smt2

All the formulas at each level in the assertion stack are satisfiable. But z3str3 gives unsat at some level. For example for the file 1.smt2, z3str3 gives:
sat
sat
unsat

while z3-seq gives:
sat
sat
sat

OS:
NAME="Ubuntu"
VERSION="16.04.5 LTS (Xenial Xerus)"

$ git log -1
commit 321bad2
Author: Christoph M. Wintersteiger cwinter@microsoft.com
Date: Mon Jan 20 17:06:35 2020 +0000
Fix for implicit consts in FPA models. Fixes #2865.

[mtrberzi]

OK, thanks for the new cases. Is that commit the one you tested on?

I'm actually in the middle of replacing the length and value testing algorithm with an improved procedure that should deal with many of these correctness issues. I tracked down several wrong-answer cases to bad behaviour in the legacy algorithm and the best way is to implement this new technique (which should also be more efficient in many cases). I'll let you know when it's ready to be tested, I would really appreciate the cross-check from your tool.

[numairmansur]

That sounds good. Just let me know when it's ready :)
and yes that is the commit on which I tested on.

[mtrberzi]

OK, all of these cases now return SAT, or time out. I'll close this issue for now, and look at addressing the slow cases after some of the bigger old issues are resolved. Please do keep reporting any wrong answer cases or crashes you find, I appreciate it.